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  180  pm2.8  966  dedlem0b  1036  meredith  1633  necon3bd  3027  necon1bd  3031  spc2d  3600  sspss  4073  neldif  4103  ssonprc  7496  limsssuc  7554  limom  7584  onfununi  7967  pw2f1olem  8609  domtriord  8651  pssnn  8724  ordtypelem10  8979  rankxpsuc  9299  carden2a  9383  fidomtri2  9411  alephdom  9495  isf32lem12  9774  isfin1-3  9796  isfin7-2  9806  entric  9967  inttsk  10184  zeo  12056  zeo2  12057  xrlttri  12520  xaddf  12605  elfzonelfzo  13127  fzonfzoufzol  13128  elfznelfzo  13130  om2uzf1oi  13309  hashnfinnn0  13710  ruclem3  15574  sumodd  15727  bitsinv1lem  15778  sadcaddlem  15794  phiprmpw  16101  iserodd  16160  fldivp1  16221  prmpwdvds  16228  vdwlem6  16310  sylow2alem2  18672  efgs1b  18791  fctop  21540  cctop  21542  ppttop  21543  iccpnfcnv  23475  iccpnfhmeo  23476  iscau2  23807  ovolicc2lem2  24046  mbfeqalem1  24169  limccnp2  24417  radcnv0  24931  psercnlem1  24940  pserdvlem2  24943  logtayl  25170  cxpsqrt  25213  rlimcnp2  25471  amgm  25495  pntpbnd1  26089  pntlem3  26112  atssma  30082  fsuppcurry1  30387  fsuppcurry2  30388  supxrnemnf  30419  xrge0iifcnv  31075  eulerpartlemf  31527  cusgracyclt3v  32300  nolesgn2o  33075  arg-ax  33661  pw2f1ocnv  39512  infordmin  39777  clsk1independent  40274  pm10.57  40580  con5  40733  con3ALT2  40741  xrred  41509  afvco2  43252  islininds2  44467
  Copyright terms: Public domain W3C validator