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  5552  sotrieq  5553  sotr2  5556  isso2i  5559  sotr3  5563  sotri2  6075  sotri3  6076  somin1  6079  somincom  6080  ordtri2  6341  ordtr3  6352  ordintdif  6357  ord0eln0  6362  soisoi  7262  weniso  7288  ordunisuc2  7774  limsssuc  7780  nlimon  7781  tfrlem15  8311  oawordeulem  8469  nnawordex  8552  fimaxg  9171  suplub2  9345  fiming  9384  wemapsolem  9436  cantnflem1  9579  rankval3b  9719  cardsdomel  9867  harsdom  9888  isfin1-2  10276  fin1a2lem7  10297  suplem2pr  10944  xrltnle  11179  ltnle  11192  leloe  11199  xrlttri  13038  xrleloe  13043  xrrebnd  13067  supxrbnd2  13221  supxrbnd  13227  om2uzf1oi  13860  rabssnn0fi  13893  cnpart  15147  bits0e  16340  bitsmod  16347  bitsinv1lem  16352  sadcaddlem  16368  trfil2  23802  xrsxmet  24725  metdsge  24765  ovolunlem1a  25424  ovolunlem1  25425  itg2seq  25670  noetasuplem4  27675  noetainflem4  27679  sltnle  27692  sleloe  27693  sgnneg  32816  toslublem  32953  tosglblem  32955  isarchi2  33154  gsumesum  34072  elfuns  35957  finminlem  36360  bj-bibibi  36628  itg2addnclem  37719  heiborlem10  37868  aks4d1p8  42128  cantnfresb  43365  naddwordnexlem4  43442  ontric3g  43563  or3or  44064  ntrclselnel2  44099  clsneifv3  44151  islininds2  48524  resinsnlem  48910