Theorem con2bid 355

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 354	. 2 ⊢ ((𝜒 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜒))
3	1, 2	sylibr 235	1 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))

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

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 208

This theorem is referenced by:  con1bid  356  sotric  5556  sotrieq  5557  sotr2  5560  isso2i  5563  sotr3  5567  sotri2  6079  sotri3  6080  somin1  6083  somincom  6084  ordtri2  6345  ordtr3  6356  ordintdif  6361  ord0eln0  6366  soisoi  7272  weniso  7298  ordunisuc2  7784  limsssuc  7790  nlimon  7791  tfrlem15  8321  oawordeulem  8479  nnawordex  8563  fimaxg  9187  suplub2  9364  fiming  9403  wemapsolem  9455  cantnflem1  9601  rankval3b  9741  cardsdomel  9889  harsdom  9910  isfin1-2  10298  fin1a2lem7  10319  suplem2pr  10967  xrltnle  11203  ltnle  11216  leloe  11223  xrlttri  13081  xrleloe  13086  xrrebnd  13111  supxrbnd2  13265  supxrbnd  13271  om2uzf1oi  13906  rabssnn0fi  13939  cnpart  15193  bits0e  16389  bitsmod  16396  bitsinv1lem  16401  sadcaddlem  16417  trfil2  23870  xrsxmet  24793  metdsge  24833  ovolunlem1a  25481  ovolunlem1  25482  itg2seq  25727  noetasuplem4  27718  noetainflem4  27722  ltnles  27735  lesloe  27736  sgnneg  32925  toslublem  33051  tosglblem  33053  isarchi2  33266  gsumesum  34243  elfuns  36141  finminlem  36546  bj-bibibi  36897  itg2addnclem  38038  heiborlem10  38187  aks4d1p8  42572  cantnfresb  43769  naddwordnexlem4  43846  ontric3g  43966  or3or  44467  ntrclselnel2  44502  clsneifv3  44554  islininds2  48975  resinsnlem  49361