Theorem con2bid 355

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

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

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 206

This theorem is referenced by:  con1bid  356  sotric  5532  sotrieq  5533  sotr2  5536  isso2i  5539  sotri2  6039  sotri3  6040  somin1  6043  somincom  6044  ordtri2  6305  ordtr3  6315  ordintdif  6319  ord0eln0  6324  soisoi  7208  weniso  7234  ordunisuc2  7700  limsssuc  7706  nlimon  7707  tfrlem15  8232  oawordeulem  8394  nnawordex  8477  onomeneqOLD  9021  fimaxg  9070  suplub2  9229  fiming  9266  wemapsolem  9318  cantnflem1  9456  rankval3b  9593  cardsdomel  9741  harsdom  9762  isfin1-2  10150  fin1a2lem7  10171  suplem2pr  10818  xrltnle  11051  ltnle  11063  leloe  11070  xrlttri  12882  xrleloe  12887  xrrebnd  12911  supxrbnd2  13065  supxrbnd  13071  om2uzf1oi  13682  rabssnn0fi  13715  cnpart  14960  bits0e  16145  bitsmod  16152  bitsinv1lem  16157  sadcaddlem  16173  trfil2  23047  xrsxmet  23981  metdsge  24021  ovolunlem1a  24669  ovolunlem1  24670  itg2seq  24916  toslublem  31259  tosglblem  31261  isarchi2  31448  gsumesum  32036  sgnneg  32516  sotr3  33742  noetasuplem4  33948  noetainflem4  33952  sltnle  33965  sleloe  33966  elfuns  34226  finminlem  34516  bj-bibibi  34777  itg2addnclem  35837  heiborlem10  35987  aks4d1p8  40102  ontric3g  41136  or3or  41638  ntrclselnel2  41675  clsneifv3  41727  islininds2  45836