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  5563  sotrieq  5564  sotr2  5567  isso2i  5570  sotr3  5574  sotri2  6087  sotri3  6088  somin1  6091  somincom  6092  ordtri2  6353  ordtr3  6364  ordintdif  6369  ord0eln0  6374  soisoi  7277  weniso  7303  ordunisuc2  7789  limsssuc  7795  nlimon  7796  tfrlem15  8325  oawordeulem  8483  nnawordex  8567  fimaxg  9191  suplub2  9368  fiming  9407  wemapsolem  9459  cantnflem1  9604  rankval3b  9744  cardsdomel  9892  harsdom  9913  isfin1-2  10301  fin1a2lem7  10322  suplem2pr  10970  xrltnle  11206  ltnle  11219  leloe  11226  xrlttri  13084  xrleloe  13089  xrrebnd  13114  supxrbnd2  13268  supxrbnd  13274  om2uzf1oi  13909  rabssnn0fi  13942  cnpart  15196  bits0e  16392  bitsmod  16399  bitsinv1lem  16404  sadcaddlem  16420  trfil2  23865  xrsxmet  24788  metdsge  24828  ovolunlem1a  25476  ovolunlem1  25477  itg2seq  25722  noetasuplem4  27717  noetainflem4  27721  ltnles  27734  lesloe  27735  sgnneg  32924  toslublem  33050  tosglblem  33052  isarchi2  33264  gsumesum  34222  elfuns  36114  finminlem  36519  bj-bibibi  36870  itg2addnclem  38009  heiborlem10  38158  aks4d1p8  42543  cantnfresb  43773  naddwordnexlem4  43850  ontric3g  43970  or3or  44471  ntrclselnel2  44506  clsneifv3  44558  islininds2  48975  resinsnlem  49361