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  5601  sotrieq  5602  sotr2  5605  isso2i  5608  sotr3  5612  sotri2  6131  sotri3  6132  somin1  6135  somincom  6136  ordtri2  6400  ordtr3  6411  ordintdif  6416  ord0eln0  6421  soisoi  7335  weniso  7363  ordunisuc2  7846  limsssuc  7852  nlimon  7853  tfrlem15  8385  oawordeulem  8545  nnawordex  8629  fimaxg  9254  suplub2  9428  fiming  9467  wemapsolem  9519  cantnflem1  9665  rankval3b  9805  cardsdomel  9976  harsdom  9997  isfin1-2  10384  fin1a2lem7  10405  suplem2pr  11053  xrltnle  11291  ltnle  11304  leloe  11311  xrlttri  13180  xrleloe  13185  xrrebnd  13210  supxrbnd2  13364  supxrbnd  13370  om2uzf1oi  14007  rabssnn0fi  14040  sgnneg  15161  cnpart  15315  bits0e  16509  bitsmod  16516  bitsinv1lem  16521  sadcaddlem  16537  trfil2  24095  xrsxmet  25018  metdsge  25058  ovolunlem1a  25706  ovolunlem1  25707  itg2seq  25952  noetasuplem4  27951  noetainflem4  27955  ltnles  27968  lesloe  27969  toslublem  33356  tosglblem  33358  isarchi2  33569  gsumesum  34513  elfuns  36442  naddle  36748  finminlem  36886  bj-bibibi  37236  itg2addnclem  38379  heiborlem10  38529  aks4d1p8  42912  cantnfresb  44109  naddwordnexlem4  44186  ontric3g  44306  or3or  44807  ntrclselnel2  44842  clsneifv3  44894  islininds2  49321  resinsnlem  49706