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  5596  sotrieq  5597  sotr2  5600  isso2i  5603  sotr3  5607  sotri2  6141  sotri3  6142  somin1  6145  somincom  6146  ordtri2  6424  ordtr3  6435  ordintdif  6440  ord0eln0  6445  soisoi  7367  weniso  7395  ordunisuc2  7889  limsssuc  7895  nlimon  7896  tfrlem15  8438  oawordeulem  8600  nnawordex  8684  fimaxg  9316  suplub2  9490  fiming  9529  wemapsolem  9581  cantnflem1  9727  rankval3b  9873  cardsdomel  10092  harsdom  10115  isfin1-2  10502  fin1a2lem7  10523  suplem2pr  11177  xrltnle  11415  ltnle  11428  leloe  11435  xrlttri  13308  xrleloe  13313  xrrebnd  13338  supxrbnd2  13492  supxrbnd  13498  om2uzf1oi  14136  rabssnn0fi  14169  sgnneg  15296  cnpart  15450  bits0e  16643  bitsmod  16650  bitsinv1lem  16655  sadcaddlem  16671  trfil2  24261  xrsxmet  25184  metdsge  25224  ovolunlem1a  25872  ovolunlem1  25873  itg2seq  26118  noetasuplem4  28150  noetainflem4  28154  ltnles  28167  lesloe  28168  toslublem  33629  tosglblem  33631  isarchi2  33845  gsumesum  34802  infinfnum  35890  elfuns  36892  naddle  37183  finminlem  37321  bj-bibibi  37671  itg2addnclem  38857  heiborlem10  39020  aks4d1p8  43403  cantnfresb  44587  naddwordnexlem4  44664  ontric3g  44784  or3or  45284  ntrclselnel2  45319  clsneifv3  45371  islininds2  49927  resinsnlem  50315