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  5621  sotrieq  5622  sotr2  5625  isso2i  5628  sotr3  5632  sotri2  6148  sotri3  6149  somin1  6152  somincom  6153  ordtri2  6418  ordtr3  6428  ordintdif  6433  ord0eln0  6438  soisoi  7349  weniso  7375  ordunisuc2  7866  limsssuc  7872  nlimon  7873  tfrlem15  8433  oawordeulem  8593  nnawordex  8676  onomeneqOLD  9267  fimaxg  9324  suplub2  9502  fiming  9539  wemapsolem  9591  cantnflem1  9730  rankval3b  9867  cardsdomel  10015  harsdom  10036  isfin1-2  10426  fin1a2lem7  10447  suplem2pr  11094  xrltnle  11329  ltnle  11341  leloe  11348  xrlttri  13182  xrleloe  13187  xrrebnd  13211  supxrbnd2  13365  supxrbnd  13371  om2uzf1oi  13995  rabssnn0fi  14028  cnpart  15280  bits0e  16467  bitsmod  16474  bitsinv1lem  16479  sadcaddlem  16495  trfil2  23896  xrsxmet  24832  metdsge  24872  ovolunlem1a  25532  ovolunlem1  25533  itg2seq  25778  noetasuplem4  27782  noetainflem4  27786  sltnle  27799  sleloe  27800  toslublem  32963  tosglblem  32965  isarchi2  33193  gsumesum  34061  sgnneg  34544  elfuns  35917  finminlem  36320  bj-bibibi  36588  itg2addnclem  37679  heiborlem10  37828  aks4d1p8  42089  cantnfresb  43342  naddwordnexlem4  43419  ontric3g  43540  or3or  44041  ntrclselnel2  44076  clsneifv3  44128  islininds2  48406  resinsnlem  48777