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  848  dedlem0b  951  meredith  1456  hbnt  1842  axc11nlem  1885  axc11nlemOLD  2021  necon3bd  2679  necon1adOLD  2684  necon1bd  2685  necon4bdOLD  2690  sspss  3603  neldif  3629  ssonprc  6611  limsssuc  6669  limom  6699  onfununi  7012  pw2f1olem  7621  domtriord  7663  pssnn  7738  ordtypelem10  7952  rankxpsuc  8300  carden2a  8347  fidomtri2  8375  alephdom  8462  isf32lem12  8744  isfin1-3  8766  isfin7-2  8776  entric  8932  inttsk  9152  zeo  10946  zeo2  10947  uzwoOLD  11145  xrlttri  11345  xaddf  11423  elfzonelfzo  11880  fzonfzoufzol  11881  elfznelfzo  11883  om2uzf1oi  12032  hashnfinnn0  12400  ruclem3  13827  bitsinv1lem  13950  sadcaddlem  13966  phiprmpw  14165  iserodd  14218  fldivp1  14275  prmpwdvds  14281  vdwlem6  14363  sylow2alem2  16444  efgs1b  16560  fctop  19299  cctop  19301  ppttop  19302  iccpnfcnv  21207  iccpnfhmeo  21208  iscau2  21479  ovolicc2lem2  21692  mbfeqalem  21812  limccnp2  22059  radcnv0  22573  psercnlem1  22582  pserdvlem2  22585  logtayl  22797  cxpsqrt  22840  leibpilem1  23027  rlimcnp2  23052  amgm  23076  pntpbnd1  23527  pntlem3  23550  atssma  27001  spc2d  27077  supxrnemnf  27279  xrge0iifcnv  27579  eulerpartlemf  27977  arg-ax  29486  pw2f1ocnv  30611  pm10.57  30882  afvco2  31756  islininds2  32184  con5  32389  con3ALT  32397  bj-axc11nlemv  33414