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

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

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 207

This theorem is referenced by:  con1bid  355  sotric  5569  sotrieq  5570  sotr2  5573  isso2i  5576  sotr3  5580  sotri2  6092  sotri3  6093  somin1  6096  somincom  6097  ordtri2  6358  ordtr3  6369  ordintdif  6374  ord0eln0  6379  soisoi  7283  weniso  7309  ordunisuc2  7795  limsssuc  7801  nlimon  7802  tfrlem15  8331  oawordeulem  8489  nnawordex  8573  fimaxg  9197  suplub2  9374  fiming  9413  wemapsolem  9465  cantnflem1  9610  rankval3b  9750  cardsdomel  9898  harsdom  9919  isfin1-2  10307  fin1a2lem7  10328  suplem2pr  10976  xrltnle  11212  ltnle  11225  leloe  11232  xrlttri  13090  xrleloe  13095  xrrebnd  13120  supxrbnd2  13274  supxrbnd  13280  om2uzf1oi  13915  rabssnn0fi  13948  cnpart  15202  bits0e  16398  bitsmod  16405  bitsinv1lem  16410  sadcaddlem  16426  trfil2  23852  xrsxmet  24775  metdsge  24815  ovolunlem1a  25463  ovolunlem1  25464  itg2seq  25709  noetasuplem4  27700  noetainflem4  27704  ltnles  27717  lesloe  27718  sgnneg  32906  toslublem  33032  tosglblem  33034  isarchi2  33246  gsumesum  34203  elfuns  36095  finminlem  36500  bj-bibibi  36851  itg2addnclem  37992  heiborlem10  38141  aks4d1p8  42526  cantnfresb  43752  naddwordnexlem4  43829  ontric3g  43949  or3or  44450  ntrclselnel2  44485  clsneifv3  44537  islininds2  48960  resinsnlem  49346