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

Theorem con2d 136
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
con2d (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d
StepHypRef Expression
1 notnotr 132 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 34 . 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:  con2  137  mt2d  138  pm3.2im  162  exists2  2749  exists2OLD  2750  necon2bd  3037  spcimegf  3594  spcegf  3596  spcimedv  3599  rspcimedv  3618  disjxun  5061  sotric  5500  sotrieq  5501  poirr2  5982  funun  6397  imadif  6435  soisoi  7073  onnminsb  7507  oneqmin  7508  ordunisuc2  7547  limsssuc  7553  wfrlem10  7955  tz7.48lem  8068  sdomdif  8654  pssinf  8717  unblem1  8759  supnub  8915  infnlb  8945  elirrv  9049  inf3lem6  9085  cantnflem1  9141  cardne  9383  cardsdomel  9392  carddom2  9395  cardmin2  9416  alephnbtwn  9486  infdif2  9621  fin4en1  9720  fin23lem31  9754  isf32lem5  9768  isf34lem4  9788  cfpwsdom  9995  fpwwe2  10054  addnidpi  10312  genpnnp  10416  btwnnz  12047  prime  12052  qsqueeze  12584  xralrple  12588  xmullem2  12648  xmulneg1  12652  ssfzoulel  13121  elfznelfzob  13133  bcval4  13657  seqcoll  13812  hashtpg  13833  swrd0  14010  fsumcvg  15059  fsumsplit  15087  fprodcvg  15274  fprodsplit  15310  dvdsle  15650  divalglem8  15741  bitsinv1lem  15780  2mulprm  16027  pockthg  16232  prmunb  16240  vdwlem6  16312  ramlb  16345  gsumzsplit  18967  opsrtoslem2  20184  obselocv  20791  elcls  21600  fbasrn  22411  ufilb  22433  ufilmax  22434  rnelfmlem  22479  alexsubALTlem4  22577  tsmssplit  22678  recld2  23340  logbgcd1irr  25288  fsumharmonic  25506  chtub  25705  lgsne0  25828  axlowdim  26664  wlkp1lem5  27376  wlkp1lem6  27377  cyclnspth  27498  eupth2lem3lem4  27927  cvnsym  29984  cvntr  29986  atcvati  30080  rmounid  30176  ballotlemfc0  31639  ballotlemfcc  31640  ballotlemfrcn0  31676  ballotlemirc  31678  acycgr2v  32284  cusgracyclt3v  32290  fmlasucdisj  32533  dfpo2  32878  sltres  33056  nosupbnd2lem1  33102  nocvxminlem  33134  nn0prpw  33558  onsucconni  33672  onint1  33684  icorempo  34504  relowlpssretop  34517  fvineqsneq  34565  lindsenlbs  34757  poimirlem16  34778  poimirlem26  34788  fdc  34891  lsatcvat  36056  hlrelat2  36409  ltltncvr  36429  islln2a  36523  islpln2a  36554  islvol2aN  36598  rencldnfilem  39285  ss2iundf  39872  uneqsn  40241  radcnvrat  40514  stoweidlem34  42188  oddneven  43644
  Copyright terms: Public domain W3C validator