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  2591  necon2bd  2839  spcimegf  3318  spcegf  3320  spcimedv  3323  rspcimedv  3342  minelOLD  4067  disjxun  4683  sotric  5090  sotrieq  5091  poirr2  5555  funun  5970  imadif  6011  soisoi  6618  onnminsb  7046  oneqmin  7047  ordunisuc2  7086  limsssuc  7092  wfrlem10  7469  tz7.48lem  7581  sdomdif  8149  pssinf  8211  unblem1  8253  supnub  8409  infnlb  8439  elirrv  8542  inf3lem6  8568  cantnflem1  8624  cardne  8829  cardsdomel  8838  carddom2  8841  cardmin2  8862  alephnbtwn  8932  infdif2  9070  fin4en1  9169  fin23lem31  9203  isf32lem5  9217  isf34lem4  9237  cfpwsdom  9444  fpwwe2  9503  addnidpi  9761  genpnnp  9865  btwnnz  11491  prime  11496  qsqueeze  12070  xralrple  12074  xmullem2  12133  xmulneg1  12137  ssfzoulel  12602  elfznelfzob  12614  bcval4  13134  seqcoll  13286  hashtpg  13305  swrd0  13480  fsumcvg  14487  fsumsplit  14515  fprodcvg  14704  fprodsplit  14740  dvdsle  15079  divalglem8  15170  bitsinv1lem  15210  pockthg  15657  prmunb  15665  vdwlem6  15737  ramlb  15770  gsumzsplit  18373  opsrtoslem2  19533  obselocv  20120  elcls  20925  fbasrn  21735  ufilb  21757  ufilmax  21758  rnelfmlem  21803  alexsubALTlem4  21901  tsmssplit  22002  recld2  22664  fsumharmonic  24783  chtub  24982  lgsne0  25105  axlowdim  25886  nbgrssovtxOLD  26305  wlkp1lem5  26630  wlkp1lem6  26631  cyclnspth  26751  eupth2lem3lem4  27209  cvnsym  29277  cvntr  29279  atcvati  29373  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfrcn0  30719  ballotlemirc  30721  dfpo2  31771  sltres  31940  nosupbnd2lem1  31986  nocvxminlem  32018  nn0prpw  32443  onsucconni  32561  onint1  32573  icorempt2  33329  relowlpssretop  33342  lindsenlbs  33534  poimirlem16  33555  poimirlem26  33565  fdc  33671  lsatcvat  34655  hlrelat2  35007  ltltncvr  35027  islln2a  35121  islpln2a  35152  islvol2aN  35196  rencldnfilem  37701  ss2iundf  38268  uneqsn  38638  radcnvrat  38830  stoweidlem34  40569  oddneven  41882
  Copyright terms: Public domain W3C validator