Theorem con1d 127

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 125	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 34	. 2 |- ( ph -> ( -. ps -> -. -. ch ) )
4	3	con4d 108	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  128  con1  131  pm2.24d  137  con3d  138  pm2.61d  161  pm2.8  858  dedlem0b  961  meredith  1519  hbnt  1951  axc11nlem  1996  axc11nlemOLD  2104  necon3bd  2643  necon1adOLD  2648  necon1bd  2649  necon4bdOLD  2654  sspss  3570  neldif  3596  ssonprc  6633  limsssuc  6691  limom  6721  onfununi  7068  pw2f1olem  7682  domtriord  7724  pssnn  7796  ordtypelem10  8042  rankxpsuc  8352  carden2a  8399  fidomtri2  8427  alephdom  8510  isf32lem12  8792  isfin1-3  8814  isfin7-2  8824  entric  8980  inttsk  9198  zeo  11021  zeo2  11022  xrlttri  11438  xaddf  11517  elfzonelfzo  12008  fzonfzoufzol  12009  elfznelfzo  12011  om2uzf1oi  12164  hashnfinnn0  12539  ruclem3  14263  bitsinv1lem  14389  sadcaddlem  14405  phiprmpw  14693  iserodd  14748  fldivp1  14805  prmpwdvds  14811  vdwlem6  14899  sylow2alem2  17205  efgs1b  17321  fctop  19950  cctop  19952  ppttop  19953  iccpnfcnv  21868  iccpnfhmeo  21869  iscau2  22140  ovolicc2lem2  22349  mbfeqalem  22475  limccnp2  22724  radcnv0  23236  psercnlem1  23245  pserdvlem2  23248  logtayl  23470  cxpsqrt  23513  leibpilem1  23731  rlimcnp2  23757  amgm  23781  pntpbnd1  24287  pntlem3  24310  atssma  27866  spc2d  27942  supxrnemnf  28190  xrge0iifcnv  28578  eulerpartlemf  29029  arg-ax  30861  bj-axc11nlemv  31095  pw2f1ocnv  35598  pm10.57  36357  con5  36516  con3ALT  36524  afvco2  38068  islininds2  39037