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 4514  cardaleph 4885  suplem2pr 5162  elnnz 6145  elnnz1 6155  fzneuzt 6518  infpnlem1 7506  top2usne 10549  filintf 10569

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

Copyright terms: Public domain