Theorem con2bid 357

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

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

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 210

This theorem is referenced by:  con1bid  358  sotric  5602  sotrieq  5603  sotr2  5606  isso2i  5609  sotr3  5613  sotri2  6132  sotri3  6133  somin1  6136  somincom  6137  ordtri2  6399  ordtr3  6410  ordintdif  6415  ord0eln0  6420  soisoi  7329  weniso  7355  ordunisuc2  7842  limsssuc  7848  nlimon  7849  tfrlem15  8381  oawordeulem  8541  nnawordex  8625  fimaxg  9249  suplub2  9423  fiming  9462  wemapsolem  9514  cantnflem1  9660  rankval3b  9800  cardsdomel  9962  harsdom  9983  isfin1-2  10371  fin1a2lem7  10392  suplem2pr  11040  xrltnle  11278  ltnle  11291  leloe  11298  xrlttri  13166  xrleloe  13171  xrrebnd  13196  supxrbnd2  13350  supxrbnd  13356  om2uzf1oi  13991  rabssnn0fi  14024  sgnneg  15139  cnpart  15293  bits0e  16489  bitsmod  16496  bitsinv1lem  16501  sadcaddlem  16517  trfil2  24015  xrsxmet  24938  metdsge  24978  ovolunlem1a  25626  ovolunlem1  25627  itg2seq  25872  noetasuplem4  27868  noetainflem4  27872  ltnles  27885  lesloe  27886  toslublem  33235  tosglblem  33237  isarchi2  33448  gsumesum  34396  elfuns  36340  finminlem  36754  bj-bibibi  37104  itg2addnclem  38247  heiborlem10  38396  aks4d1p8  42781  cantnfresb  43980  naddwordnexlem4  44057  ontric3g  44177  or3or  44678  ntrclselnel2  44713  clsneifv3  44765  islininds2  49186  resinsnlem  49571