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  1936  hbnt  2024  axc11nlemOLD  2070  axc11nlemALT  2198  necon3bd  2700  necon1bd  2704  sspss  3572  neldif  3601  ssonprc  6759  limsssuc  6817  limom  6847  onfununi  7200  pw2f1olem  7824  domtriord  7866  pssnn  7938  ordtypelem10  8190  rankxpsuc  8503  carden2a  8550  fidomtri2  8578  alephdom  8662  isf32lem12  8944  isfin1-3  8966  isfin7-2  8976  entric  9133  inttsk  9350  zeo  11202  zeo2  11203  xrlttri  11716  xaddf  11797  elfzonelfzo  12303  fzonfzoufzol  12304  elfznelfzo  12306  om2uzf1oi  12481  hashnfinnn0  12877  ruclem3  14668  sumodd  14816  bitsinv1lem  14872  sadcaddlem  14888  phiprmpw  15195  iserodd  15260  fldivp1  15321  prmpwdvds  15328  vdwlem6  15410  sylow2alem2  17762  efgs1b  17878  fctop  20519  cctop  20521  ppttop  20522  iccpnfcnv  22472  iccpnfhmeo  22473  iscau2  22748  ovolicc2lem2  22969  mbfeqalem  23091  limccnp2  23338  radcnv0  23862  psercnlem1  23871  pserdvlem2  23874  logtayl  24094  cxpsqrt  24137  leibpilem1  24355  rlimcnp2  24381  amgm  24405  pntpbnd1  24965  pntlem3  24988  atssma  28410  spc2d  28486  supxrnemnf  28720  xrge0iifcnv  29104  eulerpartlemf  29567  arg-ax  31420  pw2f1ocnv  36497  clsk1independent  37246  pm10.57  37474  con5  37631  con3ALT2  37639  xrred  38408  afvco2  39800  islininds2  42159
  Copyright terms: Public domain W3C validator