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  5626  sotrieq  5627  sotr2  5630  isso2i  5633  sotr3  5637  sotri2  6152  sotri3  6153  somin1  6156  somincom  6157  ordtri2  6421  ordtr3  6431  ordintdif  6436  ord0eln0  6441  soisoi  7348  weniso  7374  ordunisuc2  7865  limsssuc  7871  nlimon  7872  tfrlem15  8431  oawordeulem  8591  nnawordex  8674  onomeneqOLD  9264  fimaxg  9321  suplub2  9499  fiming  9536  wemapsolem  9588  cantnflem1  9727  rankval3b  9864  cardsdomel  10012  harsdom  10033  isfin1-2  10423  fin1a2lem7  10444  suplem2pr  11091  xrltnle  11326  ltnle  11338  leloe  11345  xrlttri  13178  xrleloe  13183  xrrebnd  13207  supxrbnd2  13361  supxrbnd  13367  om2uzf1oi  13991  rabssnn0fi  14024  cnpart  15276  bits0e  16463  bitsmod  16470  bitsinv1lem  16475  sadcaddlem  16491  trfil2  23911  xrsxmet  24845  metdsge  24885  ovolunlem1a  25545  ovolunlem1  25546  itg2seq  25792  noetasuplem4  27796  noetainflem4  27800  sltnle  27813  sleloe  27814  toslublem  32947  tosglblem  32949  isarchi2  33175  gsumesum  34040  sgnneg  34522  elfuns  35897  finminlem  36301  bj-bibibi  36569  itg2addnclem  37658  heiborlem10  37807  aks4d1p8  42069  cantnfresb  43314  naddwordnexlem4  43391  ontric3g  43512  or3or  44013  ntrclselnel2  44048  clsneifv3  44100  islininds2  48330