Theorem con2bid 356

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

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

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 209

This theorem is referenced by:  con1bid  357  sotric  5585  sotrieq  5586  sotr2  5589  isso2i  5592  sotr3  5596  sotri2  6116  sotri3  6117  somin1  6120  somincom  6121  ordtri2  6381  ordtr3  6392  ordintdif  6397  ord0eln0  6402  soisoi  7312  weniso  7338  ordunisuc2  7824  limsssuc  7830  nlimon  7831  tfrlem15  8363  oawordeulem  8523  nnawordex  8607  fimaxg  9231  suplub2  9407  fiming  9446  wemapsolem  9498  cantnflem1  9644  rankval3b  9784  cardsdomel  9932  harsdom  9953  isfin1-2  10342  fin1a2lem7  10363  suplem2pr  11011  xrltnle  11249  ltnle  11262  leloe  11269  xrlttri  13141  xrleloe  13146  xrrebnd  13171  supxrbnd2  13325  supxrbnd  13331  om2uzf1oi  13966  rabssnn0fi  13999  sgnneg  15113  cnpart  15267  bits0e  16463  bitsmod  16470  bitsinv1lem  16475  sadcaddlem  16491  trfil2  23944  xrsxmet  24867  metdsge  24907  ovolunlem1a  25555  ovolunlem1  25556  itg2seq  25801  noetasuplem4  27797  noetainflem4  27801  ltnles  27814  lesloe  27815  toslublem  33147  tosglblem  33149  isarchi2  33362  gsumesum  34353  elfuns  36260  finminlem  36675  bj-bibibi  37026  itg2addnclem  38167  heiborlem10  38316  aks4d1p8  42701  cantnfresb  43898  naddwordnexlem4  43975  ontric3g  44095  or3or  44596  ntrclselnel2  44631  clsneifv3  44683  islininds2  49103  resinsnlem  49489