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  5593  sotrieq  5594  sotr2  5597  isso2i  5600  sotr3  5604  sotri2  6123  sotri3  6124  somin1  6127  somincom  6128  ordtri2  6393  ordtr3  6404  ordintdif  6409  ord0eln0  6414  soisoi  7329  weniso  7357  ordunisuc2  7840  limsssuc  7846  nlimon  7847  tfrlem15  8381  oawordeulem  8541  nnawordex  8625  fimaxg  9257  suplub2  9431  fiming  9470  wemapsolem  9522  cantnflem1  9668  rankval3b  9808  cardsdomel  9979  harsdom  10000  isfin1-2  10387  fin1a2lem7  10408  suplem2pr  11062  xrltnle  11300  ltnle  11313  leloe  11320  xrlttri  13190  xrleloe  13195  xrrebnd  13220  supxrbnd2  13374  supxrbnd  13380  om2uzf1oi  14017  rabssnn0fi  14050  sgnneg  15173  cnpart  15327  bits0e  16519  bitsmod  16526  bitsinv1lem  16531  sadcaddlem  16547  trfil2  24113  xrsxmet  25036  metdsge  25076  ovolunlem1a  25724  ovolunlem1  25725  itg2seq  25970  noetasuplem4  27972  noetainflem4  27976  ltnles  27989  lesloe  27990  toslublem  33412  tosglblem  33414  isarchi2  33625  gsumesum  34569  elfuns  36492  naddle  36799  finminlem  36937  bj-bibibi  37287  itg2addnclem  38420  heiborlem10  38570  aks4d1p8  42953  cantnfresb  44165  naddwordnexlem4  44242  ontric3g  44362  or3or  44863  ntrclselnel2  44898  clsneifv3  44950  islininds2  49414  resinsnlem  49797