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 692  intnanrd 693  ax6 977  equs4 1148  disjsn 2437  dfwe2 2930  ordnbtwn 3058  funun 3546  tfrlem13 3914  oprssdm 4033  php2 4500  cardaleph 4865  suplem2pr 5142  elnnz 6100  elnnz1 6110  fzneuzt 6458  infpnlem1 7457  filintf 10479

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

Copyright terms: Public domain