Theorem con2bid 353

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

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

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 206

This theorem is referenced by:  con1bid  354  sotric  5615  sotrieq  5616  sotr2  5619  isso2i  5622  sotr3  5626  sotri2  6129  sotri3  6130  somin1  6133  somincom  6134  ordtri2  6398  ordtr3  6408  ordintdif  6413  ord0eln0  6418  soisoi  7327  weniso  7353  ordunisuc2  7835  limsssuc  7841  nlimon  7842  tfrlem15  8394  oawordeulem  8556  nnawordex  8639  onomeneqOLD  9231  fimaxg  9292  suplub2  9458  fiming  9495  wemapsolem  9547  cantnflem1  9686  rankval3b  9823  cardsdomel  9971  harsdom  9992  isfin1-2  10382  fin1a2lem7  10403  suplem2pr  11050  xrltnle  11285  ltnle  11297  leloe  11304  xrlttri  13122  xrleloe  13127  xrrebnd  13151  supxrbnd2  13305  supxrbnd  13311  om2uzf1oi  13922  rabssnn0fi  13955  cnpart  15191  bits0e  16374  bitsmod  16381  bitsinv1lem  16386  sadcaddlem  16402  trfil2  23611  xrsxmet  24545  metdsge  24585  ovolunlem1a  25245  ovolunlem1  25246  itg2seq  25492  noetasuplem4  27475  noetainflem4  27479  sltnle  27492  sleloe  27493  toslublem  32409  tosglblem  32411  isarchi2  32601  gsumesum  33355  sgnneg  33837  elfuns  35191  finminlem  35506  bj-bibibi  35767  itg2addnclem  36842  heiborlem10  36991  aks4d1p8  41258  cantnfresb  42376  naddwordnexlem4  42454  ontric3g  42575  or3or  43076  ntrclselnel2  43111  clsneifv3  43163  islininds2  47252