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 236	1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

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

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 209

This theorem is referenced by:  con1bid  358  sotric  5495  sotrieq  5496  sotr2  5499  isso2i  5502  sotri2  5983  sotri3  5984  somin1  5987  somincom  5988  ordtri2  6220  ordtr3  6230  ordintdif  6234  ord0eln0  6239  soisoi  7075  weniso  7101  ordunisuc2  7553  limsssuc  7559  nlimon  7560  tfrlem15  8022  oawordeulem  8174  nnawordex  8257  onomeneq  8702  fimaxg  8759  suplub2  8919  fiming  8956  wemapsolem  9008  cantnflem1  9146  rankval3b  9249  cardsdomel  9397  harsdom  9418  isfin1-2  9801  fin1a2lem7  9822  suplem2pr  10469  xrltnle  10702  ltnle  10714  leloe  10721  xrlttri  12526  xrleloe  12531  xrrebnd  12555  supxrbnd2  12709  supxrbnd  12715  om2uzf1oi  13315  rabssnn0fi  13348  cnpart  14593  bits0e  15772  bitsmod  15779  bitsinv1lem  15784  sadcaddlem  15800  trfil2  22489  xrsxmet  23411  metdsge  23451  ovolunlem1a  24091  ovolunlem1  24092  itg2seq  24337  toslublem  30649  tosglblem  30651  isarchi2  30809  gsumesum  31313  sgnneg  31793  sotr3  32997  noetalem3  33214  sltnle  33227  sleloe  33228  elfuns  33371  finminlem  33661  bj-bibibi  33915  itg2addnclem  34937  heiborlem10  35092  ontric3g  39881  or3or  40364  ntrclselnel2  40401  clsneifv3  40453  islininds2  44533