Theorem nsyli 136

Description: A negated syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
nsyli	|- (ph -> (th -> -. ps))

Proof of Theorem nsyli

Step	Hyp	Ref	Expression
1		nsyli.1	. . 3 |- (ph -> (ps -> ch))
2	1	con3d 111	. 2 |- (ph -> (-. ch -> -. ps))
3		nsyli.2	. 2 |- (th -> -. ch)
4	2, 3	syl5 20	1 |- (ph -> (th -> -. ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  tz7.7 3684  tz7.48-2 5166  php 5607  nndomo 5614  isfinite2 5639  ordtypelem3 5686  elirrv 5700  setind 5759  zorn2lem3 5952  alephval2 6050  bcthlem28 9304  dfon2lem6 13854  axfelem12 14042  finminlem 15367  ordtypelem3OLD 15377  heiborlem22 15976

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

Copyright terms: Public domain