Theorem con1d 139

Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.)

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		notnot 136	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 35	. 2 |- ( ph -> ( -. ps -> -. -. ch ) )
4	3	con4d 114	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  140  con1  143  pm2.24d  147  con3d  148  pm2.61d  170  pm2.8  895  dedlem0b  1001  meredith  1566  axc11nlemOLD2  1988  axc16nf  2137  hbntOLD  2145  axc11nlemOLD  2160  axc11nlemALT  2306  necon3bd  2808  necon1bd  2812  sspss  3706  neldif  3735  ssonprc  6992  limsssuc  7050  limom  7080  onfununi  7438  pw2f1olem  8064  domtriord  8106  pssnn  8178  ordtypelem10  8432  rankxpsuc  8745  carden2a  8792  fidomtri2  8820  alephdom  8904  isf32lem12  9186  isfin1-3  9208  isfin7-2  9218  entric  9379  inttsk  9596  zeo  11463  zeo2  11464  xrlttri  11972  xaddf  12055  elfzonelfzo  12570  fzonfzoufzol  12571  elfznelfzo  12573  om2uzf1oi  12752  hashnfinnn0  13152  ruclem3  14962  sumodd  15111  bitsinv1lem  15163  sadcaddlem  15179  phiprmpw  15481  iserodd  15540  fldivp1  15601  prmpwdvds  15608  vdwlem6  15690  sylow2alem2  18033  efgs1b  18149  fctop  20808  cctop  20810  ppttop  20811  iccpnfcnv  22743  iccpnfhmeo  22744  iscau2  23075  ovolicc2lem2  23286  mbfeqalem  23409  limccnp2  23656  radcnv0  24170  psercnlem1  24179  pserdvlem2  24182  logtayl  24406  cxpsqrt  24449  leibpilem1  24667  rlimcnp2  24693  amgm  24717  pntpbnd1  25275  pntlem3  25298  atssma  29237  spc2d  29313  supxrnemnf  29534  xrge0iifcnv  29979  eulerpartlemf  30432  nolesgn2o  31824  arg-ax  32415  pw2f1ocnv  37604  clsk1independent  38344  pm10.57  38570  con5  38728  con3ALT2  38736  xrred  39581  afvco2  41256  islininds2  42273