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  32779  toslublem  32915  tosglblem  32917  isarchi2  33128  gsumesum  34032  elfuns  35899  finminlem  36302  bj-bibibi  36570  itg2addnclem  37661  heiborlem10  37810  aks4d1p8  42070  cantnfresb  43307  naddwordnexlem4  43384  ontric3g  43505  or3or  44006  ntrclselnel2  44041  clsneifv3  44093  islininds2  48479  resinsnlem  48865