MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1d Structured version   Unicode version

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
StepHypRef Expression
1 con1d.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  ch ) )
2 notnot1 122 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 33 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 105 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff setvar class
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  846  dedlem0b  944  meredith  1446  hbnt  1828  axc11nlem  1996  necon3bd  2645  necon4bd  2673  necon1ad  2678  sspss  3455  neldif  3481  ssonprc  6403  limsssuc  6461  limom  6491  onfununi  6802  pw2f1olem  7415  domtriord  7457  pssnn  7531  ordtypelem10  7741  rankxpsuc  8089  carden2a  8136  fidomtri2  8164  alephdom  8251  isf32lem12  8533  isfin1-3  8555  isfin7-2  8565  entric  8721  inttsk  8941  zeo  10727  zeo2  10728  uzwoOLD  10918  xrlttri  11116  xaddf  11194  elfzonelfzo  11627  fzonfzoufzol  11628  elfznelfzo  11630  om2uzf1oi  11776  hashnfinnn0  12130  ruclem3  13515  bitsinv1lem  13637  sadcaddlem  13653  phiprmpw  13851  iserodd  13902  fldivp1  13959  prmpwdvds  13965  vdwlem6  14047  sylow2alem2  16117  efgs1b  16233  fctop  18608  cctop  18610  ppttop  18611  iccpnfcnv  20516  iccpnfhmeo  20517  iscau2  20788  ovolicc2lem2  21001  mbfeqalem  21120  limccnp2  21367  radcnv0  21881  psercnlem1  21890  pserdvlem2  21893  logtayl  22105  cxpsqr  22148  leibpilem1  22335  rlimcnp2  22360  amgm  22384  pntpbnd1  22835  pntlem3  22858  atssma  25782  spc2d  25858  supxrnemnf  26056  xrge0iifcnv  26363  eulerpartlemf  26753  arg-ax  28262  pw2f1ocnv  29386  pm10.57  29623  afvco2  30082  islininds2  31018  con5  31227  con3ALT  31235  bj-axc11nlemv  32250
  Copyright terms: Public domain W3C validator