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 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  355  sotric  5522  sotrieq  5523  sotr2  5526  isso2i  5529  sotri2  6023  sotri3  6024  somin1  6027  somincom  6028  ordtri2  6286  ordtr3  6296  ordintdif  6300  ord0eln0  6305  soisoi  7179  weniso  7205  ordunisuc2  7666  limsssuc  7672  nlimon  7673  tfrlem15  8194  oawordeulem  8347  nnawordex  8430  onomeneq  8943  fimaxg  8991  suplub2  9150  fiming  9187  wemapsolem  9239  cantnflem1  9377  rankval3b  9515  cardsdomel  9663  harsdom  9684  isfin1-2  10072  fin1a2lem7  10093  suplem2pr  10740  xrltnle  10973  ltnle  10985  leloe  10992  xrlttri  12802  xrleloe  12807  xrrebnd  12831  supxrbnd2  12985  supxrbnd  12991  om2uzf1oi  13601  rabssnn0fi  13634  cnpart  14879  bits0e  16064  bitsmod  16071  bitsinv1lem  16076  sadcaddlem  16092  trfil2  22946  xrsxmet  23878  metdsge  23918  ovolunlem1a  24565  ovolunlem1  24566  itg2seq  24812  toslublem  31152  tosglblem  31154  isarchi2  31341  gsumesum  31927  sgnneg  32407  sotr3  33639  noetasuplem4  33866  noetainflem4  33870  sltnle  33883  sleloe  33884  elfuns  34144  finminlem  34434  bj-bibibi  34695  itg2addnclem  35755  heiborlem10  35905  aks4d1p8  40023  ontric3g  41027  or3or  41520  ntrclselnel2  41557  clsneifv3  41609  islininds2  45713