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

Theorem con1d 147
Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.)
Hypothesis
Ref Expression
con1d.1 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
con1d (𝜑 → (¬ 𝜒𝜓))

Proof of Theorem con1d
StepHypRef Expression
1 con1d.1 . . 3 (𝜑 → (¬ 𝜓𝜒))
2 notnot 144 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 35 . 2 (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
43con4d 115 1 (𝜑 → (¬ 𝜒𝜓))
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:  con1  148  mt3d  150  pm2.24d  154  con3d  155  pm2.61d  181  pm2.8  968  dedlem0b  1038  meredith  1635  necon3bd  3028  necon1bd  3032  spc2d  3601  sspss  4074  neldif  4104  ssonprc  7499  limsssuc  7557  limom  7587  onfununi  7970  pw2f1olem  8613  domtriord  8655  pssnn  8728  ordtypelem10  8983  rankxpsuc  9303  carden2a  9387  fidomtri2  9415  alephdom  9499  isf32lem12  9778  isfin1-3  9800  isfin7-2  9810  entric  9971  inttsk  10188  zeo  12060  zeo2  12061  xrlttri  12524  xaddf  12609  elfzonelfzo  13131  fzonfzoufzol  13132  elfznelfzo  13134  om2uzf1oi  13313  hashnfinnn0  13714  ruclem3  15578  sumodd  15731  bitsinv1lem  15782  sadcaddlem  15798  phiprmpw  16105  iserodd  16164  fldivp1  16225  prmpwdvds  16232  vdwlem6  16314  sylow2alem2  18735  efgs1b  18854  fctop  21604  cctop  21606  ppttop  21607  iccpnfcnv  23540  iccpnfhmeo  23541  iscau2  23872  ovolicc2lem2  24111  mbfeqalem1  24234  limccnp2  24482  radcnv0  24996  psercnlem1  25005  pserdvlem2  25008  logtayl  25235  cxpsqrt  25278  rlimcnp2  25536  amgm  25560  pntpbnd1  26154  pntlem3  26177  atssma  30147  fsuppcurry1  30453  fsuppcurry2  30454  supxrnemnf  30485  xrge0iifcnv  31164  eulerpartlemf  31616  cusgracyclt3v  32391  nolesgn2o  33166  arg-ax  33752  pw2f1ocnv  39619  infordmin  39884  clsk1independent  40381  pm10.57  40688  con5  40841  con3ALT2  40849  xrred  41617  afvco2  43360  islininds2  44524
  Copyright terms: Public domain W3C validator