Theorem con2bid 358

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 357	. 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  359  sotric  5496  sotrieq  5497  sotr2  5500  isso2i  5503  sotri2  5994  sotri3  5995  somin1  5998  somincom  5999  ordtri2  6248  ordtr3  6258  ordintdif  6262  ord0eln0  6267  soisoi  7137  weniso  7163  ordunisuc2  7623  limsssuc  7629  nlimon  7630  tfrlem15  8128  oawordeulem  8282  nnawordex  8365  onomeneq  8869  fimaxg  8918  suplub2  9077  fiming  9114  wemapsolem  9166  cantnflem1  9304  rankval3b  9442  cardsdomel  9590  harsdom  9611  isfin1-2  9999  fin1a2lem7  10020  suplem2pr  10667  xrltnle  10900  ltnle  10912  leloe  10919  xrlttri  12729  xrleloe  12734  xrrebnd  12758  supxrbnd2  12912  supxrbnd  12918  om2uzf1oi  13526  rabssnn0fi  13559  cnpart  14803  bits0e  15988  bitsmod  15995  bitsinv1lem  16000  sadcaddlem  16016  trfil2  22784  xrsxmet  23706  metdsge  23746  ovolunlem1a  24393  ovolunlem1  24394  itg2seq  24640  toslublem  30969  tosglblem  30971  isarchi2  31158  gsumesum  31739  sgnneg  32219  sotr3  33452  noetasuplem4  33676  noetainflem4  33680  sltnle  33693  sleloe  33694  elfuns  33954  finminlem  34244  bj-bibibi  34505  itg2addnclem  35565  heiborlem10  35715  ontric3g  40814  or3or  41308  ntrclselnel2  41345  clsneifv3  41397  islininds2  45498