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  5569  sotrieq  5570  sotr2  5573  isso2i  5576  sotr3  5580  sotri2  6090  sotri3  6091  somin1  6094  somincom  6095  ordtri2  6355  ordtr3  6366  ordintdif  6371  ord0eln0  6376  soisoi  7285  weniso  7311  ordunisuc2  7800  limsssuc  7806  nlimon  7807  tfrlem15  8337  oawordeulem  8495  nnawordex  8578  fimaxg  9210  suplub2  9388  fiming  9427  wemapsolem  9479  cantnflem1  9618  rankval3b  9755  cardsdomel  9903  harsdom  9924  isfin1-2  10314  fin1a2lem7  10335  suplem2pr  10982  xrltnle  11217  ltnle  11229  leloe  11236  xrlttri  13075  xrleloe  13080  xrrebnd  13104  supxrbnd2  13258  supxrbnd  13264  om2uzf1oi  13894  rabssnn0fi  13927  cnpart  15182  bits0e  16375  bitsmod  16382  bitsinv1lem  16387  sadcaddlem  16403  trfil2  23807  xrsxmet  24731  metdsge  24771  ovolunlem1a  25430  ovolunlem1  25431  itg2seq  25676  noetasuplem4  27681  noetainflem4  27685  sltnle  27698  sleloe  27699  sgnneg  32808  toslublem  32944  tosglblem  32946  isarchi2  33154  gsumesum  34042  elfuns  35896  finminlem  36299  bj-bibibi  36567  itg2addnclem  37658  heiborlem10  37807  aks4d1p8  42068  cantnfresb  43306  naddwordnexlem4  43383  ontric3g  43504  or3or  44005  ntrclselnel2  44040  clsneifv3  44092  islininds2  48466  resinsnlem  48852