Theorem con2bid 345

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 344	. 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
3	1, 2	sylibr 225	1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

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

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 198

This theorem is referenced by:  con1bid  346  sotric  5258  sotrieq  5259  sotr2  5261  isso2i  5264  sotri2  5736  sotri3  5737  somin1  5740  somincom  5741  ordtri2  5971  ordtr3  5982  ordintdif  5987  ord0eln0  5992  soisoi  6802  weniso  6828  ordunisuc2  7274  limsssuc  7280  nlimon  7281  tfrlem15  7724  oawordeulem  7871  nnawordex  7954  onomeneq  8389  fimaxg  8446  suplub2  8606  fiming  8643  wemapsolem  8694  cantnflem1  8833  rankval3b  8936  cardsdomel  9083  harsdom  9104  isfin1-2  9492  fin1a2lem7  9513  suplem2pr  10160  xrltnle  10390  ltnle  10402  leloe  10409  xrlttri  12188  xrleloe  12193  xrrebnd  12217  supxrbnd2  12370  supxrbnd  12376  om2uzf1oi  12976  rabssnn0fi  13009  cnpart  14203  bits0e  15370  bitsmod  15377  bitsinv1lem  15382  sadcaddlem  15398  trfil2  21904  xrsxmet  22825  metdsge  22865  ovolunlem1a  23477  ovolunlem1  23478  itg2seq  23723  toslublem  29992  tosglblem  29994  isarchi2  30064  gsumesum  30446  sgnneg  30927  sotr3  31978  noetalem3  32186  sltnle  32199  sleloe  32200  elfuns  32343  finminlem  32633  bj-bibibi  32886  itg2addnclem  33773  heiborlem10  33930  19.9alt  34745  or3or  38819  ntrclselnel2  38856  clsneifv3  38908  islininds2  42841