Theorem con2bid 354

Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)

Hypothesis

Ref	Expression
con2bid.1	⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))

Assertion

Ref	Expression
con2bid	⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

Proof of Theorem con2bid

Step	Hyp	Ref	Expression
1		con2bid.1	. 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))
2		con2bi 353	. 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
3	1, 2	sylibr 234	1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  con1bid  355  sotric  5562  sotrieq  5563  sotr2  5566  isso2i  5569  sotr3  5573  sotri2  6086  sotri3  6087  somin1  6090  somincom  6091  ordtri2  6352  ordtr3  6363  ordintdif  6368  ord0eln0  6373  soisoi  7274  weniso  7300  ordunisuc2  7786  limsssuc  7792  nlimon  7793  tfrlem15  8323  oawordeulem  8481  nnawordex  8565  fimaxg  9187  suplub2  9364  fiming  9403  wemapsolem  9455  cantnflem1  9598  rankval3b  9738  cardsdomel  9886  harsdom  9907  isfin1-2  10295  fin1a2lem7  10316  suplem2pr  10964  xrltnle  11199  ltnle  11212  leloe  11219  xrlttri  13053  xrleloe  13058  xrrebnd  13083  supxrbnd2  13237  supxrbnd  13243  om2uzf1oi  13876  rabssnn0fi  13909  cnpart  15163  bits0e  16356  bitsmod  16363  bitsinv1lem  16368  sadcaddlem  16384  trfil2  23831  xrsxmet  24754  metdsge  24794  ovolunlem1a  25453  ovolunlem1  25454  itg2seq  25699  noetasuplem4  27704  noetainflem4  27708  ltnles  27721  lesloe  27722  sgnneg  32914  toslublem  33054  tosglblem  33056  isarchi2  33267  gsumesum  34216  elfuns  36107  finminlem  36512  bj-bibibi  36786  itg2addnclem  37872  heiborlem10  38021  aks4d1p8  42341  cantnfresb  43566  naddwordnexlem4  43643  ontric3g  43763  or3or  44264  ntrclselnel2  44299  clsneifv3  44351  islininds2  48730  resinsnlem  49116