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

Theorem con2bid 355
Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)
Hypothesis
Ref Expression
con2bid.1 (𝜑 → (𝜓 ↔ ¬ 𝜒))
Assertion
Ref Expression
con2bid (𝜑 → (𝜒 ↔ ¬ 𝜓))

Proof of Theorem con2bid
StepHypRef Expression
1 con2bid.1 . 2 (𝜑 → (𝜓 ↔ ¬ 𝜒))
2 con2bi 354 . 2 ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
31, 2sylibr 233 1 (𝜑 → (𝜒 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  con1bid  356  sotric  5574  sotrieq  5575  sotr2  5578  isso2i  5581  sotr3  5585  sotri2  6084  sotri3  6085  somin1  6088  somincom  6089  ordtri2  6353  ordtr3  6363  ordintdif  6368  ord0eln0  6373  soisoi  7274  weniso  7300  ordunisuc2  7781  limsssuc  7787  nlimon  7788  tfrlem15  8339  oawordeulem  8502  nnawordex  8585  onomeneqOLD  9174  fimaxg  9235  suplub2  9398  fiming  9435  wemapsolem  9487  cantnflem1  9626  rankval3b  9763  cardsdomel  9911  harsdom  9932  isfin1-2  10322  fin1a2lem7  10343  suplem2pr  10990  xrltnle  11223  ltnle  11235  leloe  11242  xrlttri  13059  xrleloe  13064  xrrebnd  13088  supxrbnd2  13242  supxrbnd  13248  om2uzf1oi  13859  rabssnn0fi  13892  cnpart  15126  bits0e  16310  bitsmod  16317  bitsinv1lem  16322  sadcaddlem  16338  trfil2  23241  xrsxmet  24175  metdsge  24215  ovolunlem1a  24863  ovolunlem1  24864  itg2seq  25110  noetasuplem4  27087  noetainflem4  27091  sltnle  27104  sleloe  27105  toslublem  31835  tosglblem  31837  isarchi2  32024  gsumesum  32661  sgnneg  33143  elfuns  34503  finminlem  34793  bj-bibibi  35054  itg2addnclem  36132  heiborlem10  36282  aks4d1p8  40547  cantnfresb  41661  ontric3g  41801  or3or  42302  ntrclselnel2  42337  clsneifv3  42389  islininds2  46572
  Copyright terms: Public domain W3C validator