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

Theorem con1d 139
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 136 . . 3 (𝜒 → ¬ ¬ 𝜒)
31, 2syl6 35 . 2 (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
43con4d 114 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  140  con1  143  pm2.24d  147  con3d  148  pm2.61d  170  pm2.8  894  dedlem0b  1000  meredith  1563  axc11nlemOLD2  1985  axc16nf  2133  hbntOLD  2141  axc11nlemOLD  2157  axc11nlemALT  2305  necon3bd  2804  necon1bd  2808  sspss  3690  neldif  3719  ssonprc  6954  limsssuc  7012  limom  7042  onfununi  7398  pw2f1olem  8024  domtriord  8066  pssnn  8138  ordtypelem10  8392  rankxpsuc  8705  carden2a  8752  fidomtri2  8780  alephdom  8864  isf32lem12  9146  isfin1-3  9168  isfin7-2  9178  entric  9339  inttsk  9556  zeo  11423  zeo2  11424  xrlttri  11932  xaddf  12014  elfzonelfzo  12527  fzonfzoufzol  12528  elfznelfzo  12530  om2uzf1oi  12708  hashnfinnn0  13108  ruclem3  14906  sumodd  15054  bitsinv1lem  15106  sadcaddlem  15122  phiprmpw  15424  iserodd  15483  fldivp1  15544  prmpwdvds  15551  vdwlem6  15633  sylow2alem2  17973  efgs1b  18089  fctop  20748  cctop  20750  ppttop  20751  iccpnfcnv  22683  iccpnfhmeo  22684  iscau2  23015  ovolicc2lem2  23226  mbfeqalem  23349  limccnp2  23596  radcnv0  24108  psercnlem1  24117  pserdvlem2  24120  logtayl  24340  cxpsqrt  24383  leibpilem1  24601  rlimcnp2  24627  amgm  24651  pntpbnd1  25209  pntlem3  25232  atssma  29125  spc2d  29201  supxrnemnf  29419  xrge0iifcnv  29803  eulerpartlemf  30255  arg-ax  32110  pw2f1ocnv  37123  clsk1independent  37865  pm10.57  38091  con5  38249  con3ALT2  38257  xrred  39080  afvco2  40590  islininds2  41591
  Copyright terms: Public domain W3C validator