Theorem con1d 129

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		notnot1 127	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 34	. 2 |- ( ph -> ( -. ps -> -. -. ch ) )
4	3	con4d 109	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  130  con1  133  pm2.24d  139  con3d  140  pm2.61d  163  pm2.8  866  dedlem0b  970  meredith  1535  hbnt  1987  axc11nlem  2032  axc11nlemALT  2153  necon3bd  2650  necon1bd  2654  sspss  3544  neldif  3570  ssonprc  6646  limsssuc  6704  limom  6734  onfununi  7086  pw2f1olem  7702  domtriord  7744  pssnn  7816  ordtypelem10  8068  rankxpsuc  8379  carden2a  8426  fidomtri2  8454  alephdom  8538  isf32lem12  8820  isfin1-3  8842  isfin7-2  8852  entric  9008  inttsk  9225  zeo  11050  zeo2  11051  xrlttri  11467  xaddf  11546  elfzonelfzo  12042  fzonfzoufzol  12043  elfznelfzo  12045  om2uzf1oi  12199  hashnfinnn0  12574  ruclem3  14334  bitsinv1lem  14464  sadcaddlem  14480  phiprmpw  14773  iserodd  14834  fldivp1  14891  prmpwdvds  14897  vdwlem6  14985  sylow2alem2  17319  efgs1b  17435  fctop  20068  cctop  20070  ppttop  20071  iccpnfcnv  22021  iccpnfhmeo  22022  iscau2  22296  ovolicc2lem2  22520  mbfeqalem  22647  limccnp2  22896  radcnv0  23420  psercnlem1  23429  pserdvlem2  23432  logtayl  23654  cxpsqrt  23697  leibpilem1  23915  rlimcnp2  23941  amgm  23965  pntpbnd1  24473  pntlem3  24496  atssma  28080  spc2d  28156  supxrnemnf  28403  xrge0iifcnv  28788  eulerpartlemf  29252  arg-ax  31125  bj-axc11nlemv  31392  pw2f1ocnv  35937  pm10.57  36764  con5  36923  con3ALT  36931  afvco2  38716  islininds2  40550