Theorem con3d 125

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

Hypothesis

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

Assertion

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

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		notnot2 104	. . 3 |- (-. -. ps -> ps)
2		con3d.1	. . 3 |- (ph -> (ps -> ch))
3	1, 2	syl5 28	. 2 |- (ph -> (-. -. ps -> ch))
4	3	con1d 116	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:  con3  126  con3rr3  128  nsyld  132  nsyli  133  mth8  138  pm2.52  147  pm5.21ndd  343  bija  344  con3and  428  ax12bOLD  1690  ax12olem1  1927  spime  1976  mo  2226  necon1bd  2584  rexim  2718  spcimegf  2933  spcimedv  2938  rspcimedv  2957  ssneld  3275  sscon  3400  difrab  3529  ssofss  4076  pwadjoin  4119  nnsucelrlem2  4425  nnadjoin  4520  sfinltfin  4535  vfinspsslem1  4550  phi11lem1  4595  phialllem1  4616  eqfnfv  5392  dff3  5420  ndmovg  5613  nchoicelem3  6291