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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con1bid  358  sotric  5589  sotrieq  5590  sotr2  5593  isso2i  5596  sotr3  5600  sotri2  6123  sotri3  6124  somin1  6127  somincom  6128  ordtri2  6397  ordtr3  6408  ordintdif  6413  ord0eln0  6418  soisoi  7334  weniso  7362  ordunisuc2  7853  limsssuc  7859  nlimon  7860  tfrlem15  8393  oawordeulem  8555  nnawordex  8639  fimaxg  9271  suplub2  9446  fiming  9485  wemapsolem  9537  cantnflem1  9683  rankval3b  9829  cardsdomel  10048  harsdom  10069  isfin1-2  10456  fin1a2lem7  10477  suplem2pr  11131  xrltnle  11369  ltnle  11382  leloe  11389  xrlttri  13261  xrleloe  13266  xrrebnd  13291  supxrbnd2  13445  supxrbnd  13451  om2uzf1oi  14089  rabssnn0fi  14122  sgnneg  15246  cnpart  15400  bits0e  16592  bitsmod  16599  bitsinv1lem  16604  sadcaddlem  16620  trfil2  24199  xrsxmet  25122  metdsge  25162  ovolunlem1a  25810  ovolunlem1  25811  itg2seq  26056  noetasuplem4  28086  noetainflem4  28090  ltnles  28103  lesloe  28104  toslublem  33526  tosglblem  33528  isarchi2  33739  gsumesum  34684  elfuns  36657  naddle  36948  finminlem  37086  bj-bibibi  37436  itg2addnclem  38569  heiborlem10  38734  aks4d1p8  43117  cantnfresb  44310  naddwordnexlem4  44387  ontric3g  44507  or3or  45008  ntrclselnel2  45043  clsneifv3  45095  islininds2  49565  resinsnlem  49948