MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1d Structured version   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  1413  hbnt  1799  19.9htOLD  1803  19.9tOLD  1880  ax12olem3OLD  2013  ax10lem2  2023  necon3bd  2635  necon4bd  2660  necon1ad  2665  sspss  3438  neldif  3464  ssonprc  4764  limsssuc  4822  limom  4852  onfununi  6595  pw2f1olem  7204  domtriord  7245  pssnn  7319  ordtypelem10  7486  rankxpsuc  7796  carden2a  7843  fidomtri2  7871  alephdom  7952  isf32lem12  8234  isfin1-3  8256  isfin7-2  8266  entric  8422  inttsk  8639  zeo  10345  zeo2  10346  uzwoOLD  10530  xrlttri  10722  xaddf  10800  elfznelfzo  11182  om2uzf1oi  11283  hashnfinnn0  11633  ruclem3  12822  bitsinv1lem  12943  sadcaddlem  12959  phiprmpw  13155  iserodd  13199  fldivp1  13256  prmpwdvds  13262  vdwlem6  13344  sylow2alem2  15242  efgs1b  15358  fctop  17058  cctop  17060  ppttop  17061  iccpnfcnv  18959  iccpnfhmeo  18960  iscau2  19220  ovolicc2lem2  19404  mbfeqalem  19524  limccnp2  19769  radcnv0  20322  psercnlem1  20331  pserdvlem2  20334  logtayl  20541  cxpsqr  20584  leibpilem1  20770  rlimcnp2  20795  amgm  20819  pntpbnd1  21270  pntlem3  21293  atssma  23871  supxrnemnf  24117  xrge0iifcnv  24309  arg-ax  26131  pw2f1ocnv  27062  pm10.57  27498  afvco2  27971  elfzonelfzo  28079  con5  28507  con3ALT  28515  ax12olem3aAUX7  29358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator