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 5    -> wi 6
This theorem is referenced by:  mt3d  119  con1  122  con3d  127  pm2.24d  137  pm2.61d  152  pm2.8  826  dedlem0b  924  meredith  1400  ax12o10lem12  1646  ax12olem23  1657  19.9t  1761  necon3bd  2449  necon4bd  2474  necon1ad  2479  sspss  3195  neldif  3218  ssonprc  4474  limsssuc  4532  limom  4562  onfununi  6244  pw2f1olem  6851  domtriord  6892  pssnn  6966  ordtypelem10  7126  rankxpsuc  7436  carden2a  7483  fidomtri2  7511  alephdom  7592  isf32lem12  7874  isfin1-3  7896  isfin7-2  7906  entric  8061  inttsk  8276  zeo  9976  zeo2  9977  uzwoOLD  10161  xrlttri  10352  xaddf  10429  om2uzf1oi  10894  ruclem3  12385  bitsinv1lem  12506  sadcaddlem  12522  phiprmpw  12718  iserodd  12762  fldivp1  12819  prmpwdvds  12825  vdwlem6  12907  sylow2alem2  14764  efgs1b  14880  fctop  16573  cctop  16575  ppttop  16576  iccpnfcnv  18274  iccpnfhmeo  18275  iscau2  18535  ovolicc2lem2  18709  mbfeqalem  18829  limccnp2  19074  radcnv0  19624  psercnlem1  19633  pserdvlem2  19636  logtayl  19839  cxpsqr  19882  leibpilem1  20068  rlimcnp2  20093  amgm  20117  pntpbnd1  20567  pntlem3  20590  atssma  22788  arg-ax  24029  ltl4ev  24157  phthps  24161  pw2f1ocnv  26296  pm10.57  26732  con5  27075  con3ALT  27083  a4imfK  27902  ax12o10lem12K  27956  ax12o10lem12X  27957  ax12olem23X  27981  ax12-3  28008  a12study6  28022
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator