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  5570  sotrieq  5571  sotr2  5574  isso2i  5577  sotr3  5581  sotri2  6094  sotri3  6095  somin1  6098  somincom  6099  ordtri2  6360  ordtr3  6371  ordintdif  6376  ord0eln0  6381  soisoi  7284  weniso  7310  ordunisuc2  7796  limsssuc  7802  nlimon  7803  tfrlem15  8333  oawordeulem  8491  nnawordex  8575  fimaxg  9199  suplub2  9376  fiming  9415  wemapsolem  9467  cantnflem1  9610  rankval3b  9750  cardsdomel  9898  harsdom  9919  isfin1-2  10307  fin1a2lem7  10328  suplem2pr  10976  xrltnle  11211  ltnle  11224  leloe  11231  xrlttri  13065  xrleloe  13070  xrrebnd  13095  supxrbnd2  13249  supxrbnd  13255  om2uzf1oi  13888  rabssnn0fi  13921  cnpart  15175  bits0e  16368  bitsmod  16375  bitsinv1lem  16380  sadcaddlem  16396  trfil2  23843  xrsxmet  24766  metdsge  24806  ovolunlem1a  25465  ovolunlem1  25466  itg2seq  25711  noetasuplem4  27716  noetainflem4  27720  ltnles  27733  lesloe  27734  sgnneg  32925  toslublem  33065  tosglblem  33067  isarchi2  33279  gsumesum  34237  elfuns  36129  finminlem  36534  bj-bibibi  36811  itg2addnclem  37922  heiborlem10  38071  aks4d1p8  42457  cantnfresb  43681  naddwordnexlem4  43758  ontric3g  43878  or3or  44379  ntrclselnel2  44414  clsneifv3  44466  islininds2  48844  resinsnlem  49230