Theorem con1d 124

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 122	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( -. ps -> -. -. ch ) )
4	3	con4d 105	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  125  con1  128  con3d  133  pm2.24d  143  pm2.61d  158  pm2.8  850  dedlem0b  953  meredith  1459  hbnt  1880  axc11nlem  1924  axc11nlemOLD  2034  necon3bd  2655  necon1adOLD  2660  necon1bd  2661  necon4bdOLD  2666  sspss  3588  neldif  3614  ssonprc  6612  limsssuc  6670  limom  6700  onfununi  7014  pw2f1olem  7623  domtriord  7665  pssnn  7740  ordtypelem10  7955  rankxpsuc  8303  carden2a  8350  fidomtri2  8378  alephdom  8465  isf32lem12  8747  isfin1-3  8769  isfin7-2  8779  entric  8935  inttsk  9155  zeo  10954  zeo2  10955  uzwoOLD  11154  xrlttri  11354  xaddf  11432  elfzonelfzo  11891  fzonfzoufzol  11892  elfznelfzo  11894  om2uzf1oi  12043  hashnfinnn0  12411  ruclem3  13843  bitsinv1lem  13968  sadcaddlem  13984  phiprmpw  14183  iserodd  14236  fldivp1  14293  prmpwdvds  14299  vdwlem6  14381  sylow2alem2  16512  efgs1b  16628  fctop  19378  cctop  19380  ppttop  19381  iccpnfcnv  21317  iccpnfhmeo  21318  iscau2  21589  ovolicc2lem2  21802  mbfeqalem  21922  limccnp2  22169  radcnv0  22683  psercnlem1  22692  pserdvlem2  22695  logtayl  22913  cxpsqrt  22956  leibpilem1  23143  rlimcnp2  23168  amgm  23192  pntpbnd1  23643  pntlem3  23666  atssma  27169  spc2d  27245  supxrnemnf  27455  xrge0iifcnv  27788  eulerpartlemf  28182  arg-ax  29856  pw2f1ocnv  30954  pm10.57  31230  afvco2  32099  islininds2  32815  con5  33020  con3ALT  33028  bj-axc11nlemv  34057