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

Theorem con2bid 343
 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 342 . 2 ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
31, 2sylibr 224 1 (𝜑 → (𝜒 ↔ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  con1bid  344  sotric  5090  sotrieq  5091  sotr2  5093  isso2i  5096  sotri2  5560  sotri3  5561  somin1  5564  somincom  5565  ordtri2  5796  ordtr3  5807  ordintdif  5812  ord0eln0  5817  soisoi  6618  weniso  6644  ordunisuc2  7086  limsssuc  7092  nlimon  7093  tfrlem15  7533  oawordeulem  7679  nnawordex  7762  onomeneq  8191  fimaxg  8248  suplub2  8408  fiming  8445  wemapsolem  8496  cantnflem1  8624  rankval3b  8727  cardsdomel  8838  harsdom  8859  isfin1-2  9245  fin1a2lem7  9266  suplem2pr  9913  xrltnle  10143  ltnle  10155  leloe  10162  xrlttri  12010  xrleloe  12015  xrrebnd  12037  supxrbnd2  12190  supxrbnd  12196  om2uzf1oi  12792  rabssnn0fi  12825  cnpart  14024  bits0e  15198  bitsmod  15205  bitsinv1lem  15210  sadcaddlem  15226  trfil2  21738  xrsxmet  22659  metdsge  22699  ovolunlem1a  23310  ovolunlem1  23311  itg2seq  23554  toslublem  29795  tosglblem  29797  isarchi2  29867  gsumesum  30249  sgnneg  30730  sotr3  31782  noetalem3  31990  sltnle  32003  sleloe  32004  elfuns  32147  finminlem  32437  bj-bibibi  32696  itg2addnclem  33591  heiborlem10  33749  19.9alt  34570  or3or  38636  ntrclselnel2  38673  clsneifv3  38725  islininds2  42598
 Copyright terms: Public domain W3C validator