Theorem nsyl 116

Description: A negated syllogism inference.

Hypotheses

Ref	Expression
nsyl.1	|- (ph -> -. ps)
nsyl.2	|- (ch -> ps)

Assertion

Ref	Expression
nsyl	|- (ph -> -. ch)

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. 2 |- (ph -> -. ps)
2		nsyl.2	. . 3 |- (ch -> ps)
3	2	con3i 98	. 2 |- (-. ps -> -. ch)
4	1, 3	syl 10	1 |- (ph -> -. ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  intnand 693  intnanrd 694  ax6 979  equs4 1150  disjsn 2441  dfwe2 2935  ordnbtwn 3063  funun 3554  tfrlem13 3923  oprssdm 4042  php2 4512  cardaleph 4877  suplem2pr 5154  elnnz 6133  elnnz1 6143  fzneuzt 6504  infpnlem1 7491  filintf 10528

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain