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

Theorem con1d 116
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 114 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 29 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
-.  ch ) )
43con4d 97 1  |-  ( ph  ->  ( -.  ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3d  117  con1  120  con3d  125  pm2.24d  135  pm2.61d  150  pm2.8  823  dedlem0b  919  meredith  1394  19.9ht  1738  19.9t  1794  ax12olem3  1882  necon3bd  2496  necon4bd  2521  necon1ad  2526  sspss  3288  neldif  3314  ssonprc  4599  limsssuc  4657  limom  4687  onfununi  6374  pw2f1olem  6982  domtriord  7023  pssnn  7097  ordtypelem10  7258  rankxpsuc  7568  carden2a  7615  fidomtri2  7643  alephdom  7724  isf32lem12  8006  isfin1-3  8028  isfin7-2  8038  entric  8195  inttsk  8412  zeo  10113  zeo2  10114  uzwoOLD  10298  xrlttri  10489  xaddf  10567  om2uzf1oi  11032  ruclem3  12527  bitsinv1lem  12648  sadcaddlem  12664  phiprmpw  12860  iserodd  12904  fldivp1  12961  prmpwdvds  12967  vdwlem6  13049  sylow2alem2  14945  efgs1b  15061  fctop  16757  cctop  16759  ppttop  16760  iccpnfcnv  18458  iccpnfhmeo  18459  iscau2  18719  ovolicc2lem2  18893  mbfeqalem  19013  limccnp2  19258  radcnv0  19808  psercnlem1  19817  pserdvlem2  19820  logtayl  20023  cxpsqr  20066  leibpilem1  20252  rlimcnp2  20277  amgm  20301  pntpbnd1  20751  pntlem3  20774  atssma  22974  supxrnemnf  23271  xrge0iifcnv  23330  arg-ax  24927  itg2addnc  25005  ltl4ev  25095  phthps  25099  pw2f1ocnv  27233  pm10.57  27669  afvco2  28144  elfznelfzo  28213  con5  28584  con3ALT  28592  ax12olem3aAUX7  29434  ax12-3  29726  a12study6  29740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator