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  1480  hbnt  1902  axc11nlem  1946  axc11nlemOLD  2054  necon3bd  2594  necon1adOLD  2599  necon1bd  2600  necon4bdOLD  2605  sspss  3517  neldif  3543  ssonprc  6526  limsssuc  6584  limom  6614  onfununi  6930  pw2f1olem  7540  domtriord  7582  pssnn  7654  ordtypelem10  7867  rankxpsuc  8213  carden2a  8260  fidomtri2  8288  alephdom  8375  isf32lem12  8657  isfin1-3  8679  isfin7-2  8689  entric  8845  inttsk  9063  zeo  10865  zeo2  10866  xrlttri  11266  xaddf  11344  elfzonelfzo  11811  fzonfzoufzol  11812  elfznelfzo  11814  om2uzf1oi  11967  hashnfinnn0  12334  ruclem3  13968  bitsinv1lem  14093  sadcaddlem  14109  phiprmpw  14308  iserodd  14361  fldivp1  14418  prmpwdvds  14424  vdwlem6  14506  sylow2alem2  16755  efgs1b  16871  fctop  19590  cctop  19592  ppttop  19593  iccpnfcnv  21529  iccpnfhmeo  21530  iscau2  21801  ovolicc2lem2  22014  mbfeqalem  22134  limccnp2  22381  radcnv0  22896  psercnlem1  22905  pserdvlem2  22908  logtayl  23128  cxpsqrt  23171  leibpilem1  23387  rlimcnp2  23413  amgm  23437  pntpbnd1  23888  pntlem3  23911  atssma  27413  spc2d  27490  supxrnemnf  27736  xrge0iifcnv  28069  eulerpartlemf  28492  arg-ax  30034  pw2f1ocnv  31145  pm10.57  31444  afvco2  32427  islininds2  33285  con5  33625  con3ALT  33633  bj-axc11nlemv  34662