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

Theorem con2bid 342
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 341 . 2 ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
31, 2sylibr 222 1 (𝜑 → (𝜒 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  con1bid  343  sotric  4974  sotrieq  4975  sotr2  4977  isso2i  4980  sotri2  5430  sotri3  5431  somin1  5434  somincom  5435  ordtri2  5660  ordtr3  5671  ordintdif  5676  ord0eln0  5681  iotanul  5768  soisoi  6455  weniso  6481  ordunisuc2  6913  limsssuc  6919  nlimon  6920  tfrlem15  7352  oawordeulem  7498  nnawordex  7581  onomeneq  8012  fimaxg  8069  suplub2  8227  fiming  8264  wemapsolem  8315  cantnflem1  8446  rankval3b  8549  cardsdomel  8660  harsdom  8681  isfin1-2  9067  fin1a2lem7  9088  suplem2pr  9731  xrltnle  9956  ltnle  9968  leloe  9975  xrlttri  11809  xrleloe  11814  xrrebnd  11834  supxrbnd2  11982  supxrbnd  11988  om2uzf1oi  12571  rabssnn0fi  12604  cnpart  13776  bits0e  14937  bitsmod  14944  bitsinv1lem  14949  sadcaddlem  14965  trfil2  21448  xrsxmet  22367  metdsge  22407  ovolunlem1a  23015  ovolunlem1  23016  itg2seq  23259  toslublem  28791  tosglblem  28793  isarchi2  28863  gsumesum  29241  sgnneg  29722  nodenselem7  30879  elfuns  30985  finminlem  31275  bj-bibibi  31537  itg2addnclem  32414  heiborlem10  32572  19.9alt  33053  or3or  37122  ntrclselnel2  37159  clsneifv3  37211  islininds2  42048
  Copyright terms: Public domain W3C validator