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

Theorem con2d 129
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 125 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 34 . 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:  con2  130  mt2d  131  pm3.2im  157  exists2  2688  necon2bd  2936  spcimegf  3415  spcegf  3417  spcimedv  3420  rspcimedv  3439  minelOLD  4166  disjxun  4790  sotric  5201  sotrieq  5202  poirr2  5666  funun  6081  imadif  6122  soisoi  6729  onnminsb  7157  oneqmin  7158  ordunisuc2  7197  limsssuc  7203  wfrlem10  7581  tz7.48lem  7693  sdomdif  8261  pssinf  8323  unblem1  8365  supnub  8521  infnlb  8551  elirrv  8654  inf3lem6  8691  cantnflem1  8747  cardne  8952  cardsdomel  8961  carddom2  8964  cardmin2  8985  alephnbtwn  9055  infdif2  9195  fin4en1  9294  fin23lem31  9328  isf32lem5  9342  isf34lem4  9362  cfpwsdom  9569  fpwwe2  9628  addnidpi  9886  genpnnp  9990  btwnnz  11616  prime  11621  qsqueeze  12196  xralrple  12200  xmullem2  12259  xmulneg1  12263  ssfzoulel  12727  elfznelfzob  12739  bcval4  13259  seqcoll  13411  hashtpg  13430  swrd0  13605  fsumcvg  14613  fsumsplit  14641  fprodcvg  14830  fprodsplit  14866  dvdsle  15205  divalglem8  15296  bitsinv1lem  15336  pockthg  15783  prmunb  15791  vdwlem6  15863  ramlb  15896  gsumzsplit  18498  opsrtoslem2  19658  obselocv  20245  elcls  21050  fbasrn  21860  ufilb  21882  ufilmax  21883  rnelfmlem  21928  alexsubALTlem4  22026  tsmssplit  22127  recld2  22789  fsumharmonic  24908  chtub  25107  lgsne0  25230  axlowdim  26011  nbgrssovtxOLD  26430  wlkp1lem5  26755  wlkp1lem6  26756  cyclnspth  26877  eupth2lem3lem4  27354  cvnsym  29429  cvntr  29431  atcvati  29525  ballotlemfc0  30834  ballotlemfcc  30835  ballotlemfrcn0  30871  ballotlemirc  30873  dfpo2  31923  sltres  32092  nosupbnd2lem1  32138  nocvxminlem  32170  nn0prpw  32595  onsucconni  32713  onint1  32725  icorempt2  33481  relowlpssretop  33494  lindsenlbs  33686  poimirlem16  33707  poimirlem26  33717  fdc  33823  lsatcvat  34809  hlrelat2  35161  ltltncvr  35181  islln2a  35275  islpln2a  35306  islvol2aN  35350  rencldnfilem  37855  ss2iundf  38422  uneqsn  38792  radcnvrat  38984  stoweidlem34  40723  oddneven  42036
  Copyright terms: Public domain W3C validator