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

Theorem con1d 137
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 134 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 34 . 2 (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
43con4d 112 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:  mt3d  138  con1  141  pm2.24d  145  con3d  146  pm2.61d  168  pm2.8  890  dedlem0b  991  meredith  1556  axc11nlemOLD2  1974  axc16nf  2121  hbntOLD  2129  axc11nlemOLD  2145  axc11nlemALT  2293  necon3bd  2795  necon1bd  2799  sspss  3667  neldif  3696  ssonprc  6861  limsssuc  6919  limom  6949  onfununi  7302  pw2f1olem  7926  domtriord  7968  pssnn  8040  ordtypelem10  8292  rankxpsuc  8605  carden2a  8652  fidomtri2  8680  alephdom  8764  isf32lem12  9046  isfin1-3  9068  isfin7-2  9078  entric  9235  inttsk  9452  zeo  11295  zeo2  11296  xrlttri  11807  xaddf  11888  elfzonelfzo  12391  fzonfzoufzol  12392  elfznelfzo  12394  om2uzf1oi  12569  hashnfinnn0  12965  ruclem3  14747  sumodd  14895  bitsinv1lem  14947  sadcaddlem  14963  phiprmpw  15265  iserodd  15324  fldivp1  15385  prmpwdvds  15392  vdwlem6  15474  sylow2alem2  17802  efgs1b  17918  fctop  20560  cctop  20562  ppttop  20563  iccpnfcnv  22482  iccpnfhmeo  22483  iscau2  22801  ovolicc2lem2  23010  mbfeqalem  23132  limccnp2  23379  radcnv0  23891  psercnlem1  23900  pserdvlem2  23903  logtayl  24123  cxpsqrt  24166  leibpilem1  24384  rlimcnp2  24410  amgm  24434  pntpbnd1  24992  pntlem3  25015  atssma  28427  spc2d  28503  supxrnemnf  28730  xrge0iifcnv  29113  eulerpartlemf  29565  arg-ax  31391  pw2f1ocnv  36418  clsk1independent  37160  pm10.57  37388  con5  37545  con3ALT2  37553  xrred  38319  afvco2  39703  islininds2  42062
  Copyright terms: Public domain W3C validator