Theorem nsyl4 156

Description: A negated syllogism inference. (Contributed by NM, 15-Feb-1996.)

Hypotheses

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

Assertion

Ref	Expression
nsyl4	|- ( -. ch -> ps )

Proof of Theorem nsyl4

Step	Hyp	Ref	Expression
1		nsyl4.2	. . 3 |- ( -. ph -> ch )
2	1	con1i 144	. 2 |- ( -. ch -> ph )
3		nsyl4.1	. 2 |- ( ph -> ps )
4	2, 3	syl 17	1 |- ( -. ch -> ps )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  pm5.55  939  axc7  2132  moanim  2529  moexex  2541  nfunsn  6225  mptrcl  6289  card2on  8459  carden2a  8792  wwlksnfi  26801  ax10fromc7  34180  axc5c711  34203  axc5c711to11  34206  naecoms-o  34212  axc5c4c711  38602  axc5c4c711to11  38606  afvco2  41256