Theorem con2bid 356

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

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

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 208

This theorem is referenced by:  con1bid  357  sotric  5381  sotrieq  5382  sotr2  5385  isso2i  5388  sotri2  5857  sotri3  5858  somin1  5861  somincom  5862  ordtri2  6093  ordtr3  6103  ordintdif  6107  ord0eln0  6112  soisoi  6935  weniso  6961  ordunisuc2  7406  limsssuc  7412  nlimon  7413  tfrlem15  7871  oawordeulem  8021  nnawordex  8104  onomeneq  8544  fimaxg  8601  suplub2  8761  fiming  8798  wemapsolem  8850  cantnflem1  8987  rankval3b  9090  cardsdomel  9238  harsdom  9259  isfin1-2  9642  fin1a2lem7  9663  suplem2pr  10310  xrltnle  10544  ltnle  10556  leloe  10563  xrlttri  12371  xrleloe  12376  xrrebnd  12400  supxrbnd2  12554  supxrbnd  12560  om2uzf1oi  13159  rabssnn0fi  13192  cnpart  14421  bits0e  15599  bitsmod  15606  bitsinv1lem  15611  sadcaddlem  15627  trfil2  22167  xrsxmet  23088  metdsge  23128  ovolunlem1a  23768  ovolunlem1  23769  itg2seq  24014  toslublem  30298  tosglblem  30300  isarchi2  30410  gsumesum  30891  sgnneg  31371  sotr3  32555  noetalem3  32773  sltnle  32786  sleloe  32787  elfuns  32930  finminlem  33220  bj-bibibi  33470  itg2addnclem  34420  heiborlem10  34576  ontric3g  39324  or3or  39807  ntrclselnel2  39844  clsneifv3  39896  islininds2  43973