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  2585  rexim  2719  spcimegf  2934  spcimedv  2939  rspcimedv  2958  ssneld  3276  sscon  3401  difrab  3530  ssofss  4077  pwadjoin  4120  nnsucelrlem2  4426  nnadjoin  4521  sfinltfin  4536  vfinspsslem1  4551  phi11lem1  4596  phialllem1  4617  eqfnfv  5393  dff3  5421  ndmovg  5614  nchoicelem3  6292