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  23750  xrsxmet  24674  metdsge  24714  ovolunlem1a  25373  ovolunlem1  25374  itg2seq  25619  noetasuplem4  27624  noetainflem4  27628  sltnle  27641  sleloe  27642  sgnneg  32731  toslublem  32871  tosglblem  32873  isarchi2  33112  gsumesum  34022  elfuns  35876  finminlem  36279  bj-bibibi  36547  itg2addnclem  37638  heiborlem10  37787  aks4d1p8  42048  cantnfresb  43286  naddwordnexlem4  43363  ontric3g  43484  or3or  43985  ntrclselnel2  44020  clsneifv3  44072  islininds2  48446  resinsnlem  48832