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

Theorem con1d 118
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.)
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 116 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 31 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 99 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3d  119  con1  122  con3d  127  pm2.24d  137  pm2.61d  152  pm2.8  824  dedlem0b  920  meredith  1410  19.9ht  1786  19.9tOLD  1869  ax12olem3OLD  1969  ax10lem2  1981  necon3bd  2588  necon4bd  2613  necon1ad  2618  sspss  3390  neldif  3416  ssonprc  4713  limsssuc  4771  limom  4801  onfununi  6540  pw2f1olem  7149  domtriord  7190  pssnn  7264  ordtypelem10  7430  rankxpsuc  7740  carden2a  7787  fidomtri2  7815  alephdom  7896  isf32lem12  8178  isfin1-3  8200  isfin7-2  8210  entric  8366  inttsk  8583  zeo  10288  zeo2  10289  uzwoOLD  10473  xrlttri  10665  xaddf  10743  elfznelfzo  11120  om2uzf1oi  11221  hashnfinnn0  11571  ruclem3  12760  bitsinv1lem  12881  sadcaddlem  12897  phiprmpw  13093  iserodd  13137  fldivp1  13194  prmpwdvds  13200  vdwlem6  13282  sylow2alem2  15180  efgs1b  15296  fctop  16992  cctop  16994  ppttop  16995  iccpnfcnv  18841  iccpnfhmeo  18842  iscau2  19102  ovolicc2lem2  19282  mbfeqalem  19402  limccnp2  19647  radcnv0  20200  psercnlem1  20209  pserdvlem2  20212  logtayl  20419  cxpsqr  20462  leibpilem1  20648  rlimcnp2  20673  amgm  20697  pntpbnd1  21148  pntlem3  21171  atssma  23730  supxrnemnf  23964  xrge0iifcnv  24124  arg-ax  25881  itg2addnc  25960  pw2f1ocnv  26800  pm10.57  27236  afvco2  27710  con5  27950  con3ALT  27958  ax12olem3aAUX7  28796
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator