Theorem nsyl 131

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 114	. 2 |- (-. ps -> -. ch)
4	1, 3	syl 12	1 |- (ph -> -. ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  intnand 757  intnanrd 758  ax6 1325  equs4 1510  pssn2lp 2709  disjsnOLD 3090  sotrieq 3616  ordnbtwn 3761  eufromeq3 3830  dfwe2 3861  dfwe2OLD 3862  funun 4462  oprssdm 4975  tfrlem13 5131  php2 5608  en3lp 5758  cardaleph 6033  suplem2pr 6314  elnnz 7354  elnnz1 7364  fzneuz 7697  cardfz 7719  infpnlem1 8775  filintf 10274  fgfil 10290  extbas1 10291  bnj1471 13150  divalglem6 13701  axdenselem7 14025  axfelem8 14038  axfelem9 14039  axfelem11 14041  nandsym1 14246  top2usne 14898  ivthALT 15454  supfil 15560  ufinffr 15578  fsumlt1 15831  totbndbnd 15944  prtlem90 16246  0nelqs2 16269  atombase 17003  divrngidNEW 17166

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

Copyright terms: Public domain