Theorem con2bid 343

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

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

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 196

This theorem is referenced by:  con1bid  344  sotric  4985  sotrieq  4986  sotr2  4988  isso2i  4991  sotri2  5444  sotri3  5445  somin1  5448  somincom  5449  ordtri2  5675  ordtr3  5686  ordintdif  5691  ord0eln0  5696  iotanul  5783  soisoi  6478  weniso  6504  ordunisuc2  6936  limsssuc  6942  nlimon  6943  tfrlem15  7375  oawordeulem  7521  nnawordex  7604  onomeneq  8035  fimaxg  8092  suplub2  8250  fiming  8287  wemapsolem  8338  cantnflem1  8469  rankval3b  8572  cardsdomel  8683  harsdom  8704  isfin1-2  9090  fin1a2lem7  9111  suplem2pr  9754  xrltnle  9984  ltnle  9996  leloe  10003  xrlttri  11848  xrleloe  11853  xrrebnd  11873  supxrbnd2  12024  supxrbnd  12030  om2uzf1oi  12614  rabssnn0fi  12647  cnpart  13828  bits0e  14989  bitsmod  14996  bitsinv1lem  15001  sadcaddlem  15017  trfil2  21501  xrsxmet  22420  metdsge  22460  ovolunlem1a  23071  ovolunlem1  23072  itg2seq  23315  toslublem  28998  tosglblem  29000  isarchi2  29070  gsumesum  29448  sgnneg  29929  nodenselem7  31086  elfuns  31192  finminlem  31482  bj-bibibi  31744  itg2addnclem  32631  heiborlem10  32789  19.9alt  33270  or3or  37339  ntrclselnel2  37376  clsneifv3  37428  islininds2  42067