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

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

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 210

This theorem is referenced by:  con1bid  358  sotric  5599  sotrieq  5600  sotr2  5603  isso2i  5606  sotr3  5610  sotri2  6129  sotri3  6130  somin1  6133  somincom  6134  ordtri2  6396  ordtr3  6407  ordintdif  6412  ord0eln0  6417  soisoi  7326  weniso  7352  ordunisuc2  7836  limsssuc  7842  nlimon  7843  tfrlem15  8375  oawordeulem  8535  nnawordex  8619  fimaxg  9243  suplub2  9417  fiming  9456  wemapsolem  9508  cantnflem1  9654  rankval3b  9794  cardsdomel  9956  harsdom  9977  isfin1-2  10364  fin1a2lem7  10385  suplem2pr  11033  xrltnle  11271  ltnle  11284  leloe  11291  xrlttri  13159  xrleloe  13164  xrrebnd  13189  supxrbnd2  13343  supxrbnd  13349  om2uzf1oi  13985  rabssnn0fi  14018  sgnneg  15133  cnpart  15287  bits0e  16482  bitsmod  16489  bitsinv1lem  16494  sadcaddlem  16510  trfil2  24044  xrsxmet  24967  metdsge  25007  ovolunlem1a  25655  ovolunlem1  25656  itg2seq  25901  noetasuplem4  27900  noetainflem4  27904  ltnles  27917  lesloe  27918  toslublem  33292  tosglblem  33294  isarchi2  33505  gsumesum  34449  elfuns  36405  naddle  36696  finminlem  36829  bj-bibibi  37179  itg2addnclem  38322  heiborlem10  38471  aks4d1p8  42854  cantnfresb  44051  naddwordnexlem4  44128  ontric3g  44248  or3or  44749  ntrclselnel2  44784  clsneifv3  44836  islininds2  49264  resinsnlem  49649