Theorem con2bid 357

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con1bid  358  sotric  5589  sotrieq  5590  sotr2  5593  isso2i  5596  sotr3  5600  sotri2  6125  sotri3  6126  somin1  6129  somincom  6130  ordtri2  6401  ordtr3  6412  ordintdif  6417  ord0eln0  6422  soisoi  7340  weniso  7368  ordunisuc2  7859  limsssuc  7865  nlimon  7866  tfrlem15  8407  oawordeulem  8569  nnawordex  8653  fimaxg  9285  suplub2  9460  fiming  9499  wemapsolem  9551  cantnflem1  9697  rankval3b  9843  cardsdomel  10062  harsdom  10083  isfin1-2  10470  fin1a2lem7  10491  suplem2pr  11145  xrltnle  11383  ltnle  11396  leloe  11403  xrlttri  13275  xrleloe  13280  xrrebnd  13305  supxrbnd2  13459  supxrbnd  13465  om2uzf1oi  14103  rabssnn0fi  14136  sgnneg  15262  cnpart  15416  bits0e  16608  bitsmod  16615  bitsinv1lem  16620  sadcaddlem  16636  trfil2  24215  xrsxmet  25138  metdsge  25178  ovolunlem1a  25826  ovolunlem1  25827  itg2seq  26072  noetasuplem4  28102  noetainflem4  28106  ltnles  28119  lesloe  28120  toslublem  33583  tosglblem  33585  isarchi2  33796  gsumesum  34741  infinfnum  35817  elfuns  36773  naddle  37064  finminlem  37202  bj-bibibi  37552  itg2addnclem  38698  heiborlem10  38863  aks4d1p8  43246  cantnfresb  44435  naddwordnexlem4  44512  ontric3g  44632  or3or  45132  ntrclselnel2  45167  clsneifv3  45219  islininds2  49704  resinsnlem  50092