Theorem con1d 116

Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
con1d	|- (ph -> (-. ch -> ps))

Proof of Theorem con1d

Step	Hyp	Ref	Expression
1		con1d.1	. . 3 |- (ph -> (-. ps -> ch))
2		notnot1 114	. . 3 |- (ch -> -. -. ch)
3	1, 2	syl6 29	. 2 |- (ph -> (-. ps -> -. -. ch))
4	3	con4d 97	1 |- (ph -> (-. 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:  mt3d  117  con1  120  con3d  125  pm2.24d  135  pm2.61d  150  pm2.8  823  dedlem0b  919  meredith  1404  19.9ht  1778  19.9tOLD  1857  ax12olem3  1929  necon3bd  2554  necon4bd  2579  necon1ad  2584  sspss  3369  neldif  3392  nnsucelr  4429  funiunfv  5468