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  5557  sotrieq  5558  sotr2  5561  isso2i  5564  sotr3  5568  sotri2  6078  sotri3  6079  somin1  6082  somincom  6083  ordtri2  6342  ordtr3  6353  ordintdif  6358  ord0eln0  6363  soisoi  7265  weniso  7291  ordunisuc2  7777  limsssuc  7783  nlimon  7784  tfrlem15  8314  oawordeulem  8472  nnawordex  8555  fimaxg  9176  suplub2  9351  fiming  9390  wemapsolem  9442  cantnflem1  9585  rankval3b  9722  cardsdomel  9870  harsdom  9891  isfin1-2  10279  fin1a2lem7  10300  suplem2pr  10947  xrltnle  11182  ltnle  11195  leloe  11202  xrlttri  13041  xrleloe  13046  xrrebnd  13070  supxrbnd2  13224  supxrbnd  13230  om2uzf1oi  13860  rabssnn0fi  13893  cnpart  15147  bits0e  16340  bitsmod  16347  bitsinv1lem  16352  sadcaddlem  16368  trfil2  23772  xrsxmet  24696  metdsge  24736  ovolunlem1a  25395  ovolunlem1  25396  itg2seq  25641  noetasuplem4  27646  noetainflem4  27650  sltnle  27663  sleloe  27664  sgnneg  32778  toslublem  32914  tosglblem  32916  isarchi2  33127  gsumesum  34026  elfuns  35889  finminlem  36292  bj-bibibi  36560  itg2addnclem  37651  heiborlem10  37800  aks4d1p8  42060  cantnfresb  43297  naddwordnexlem4  43374  ontric3g  43495  or3or  43996  ntrclselnel2  44031  clsneifv3  44083  islininds2  48469  resinsnlem  48855