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  5637  sotrieq  5638  sotr2  5641  isso2i  5644  sotr3  5648  sotri2  6161  sotri3  6162  somin1  6165  somincom  6166  ordtri2  6430  ordtr3  6440  ordintdif  6445  ord0eln0  6450  soisoi  7364  weniso  7390  ordunisuc2  7881  limsssuc  7887  nlimon  7888  tfrlem15  8448  oawordeulem  8610  nnawordex  8693  onomeneqOLD  9292  fimaxg  9351  suplub2  9530  fiming  9567  wemapsolem  9619  cantnflem1  9758  rankval3b  9895  cardsdomel  10043  harsdom  10064  isfin1-2  10454  fin1a2lem7  10475  suplem2pr  11122  xrltnle  11357  ltnle  11369  leloe  11376  xrlttri  13201  xrleloe  13206  xrrebnd  13230  supxrbnd2  13384  supxrbnd  13390  om2uzf1oi  14004  rabssnn0fi  14037  cnpart  15289  bits0e  16475  bitsmod  16482  bitsinv1lem  16487  sadcaddlem  16503  trfil2  23916  xrsxmet  24850  metdsge  24890  ovolunlem1a  25550  ovolunlem1  25551  itg2seq  25797  noetasuplem4  27799  noetainflem4  27803  sltnle  27816  sleloe  27817  toslublem  32945  tosglblem  32947  isarchi2  33165  gsumesum  34023  sgnneg  34505  elfuns  35879  finminlem  36284  bj-bibibi  36552  itg2addnclem  37631  heiborlem10  37780  aks4d1p8  42044  cantnfresb  43286  naddwordnexlem4  43363  ontric3g  43484  or3or  43985  ntrclselnel2  44020  clsneifv3  44072  islininds2  48213