Theorem con2bid 353

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

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

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 206

This theorem is referenced by:  con1bid  354  sotric  5621  sotrieq  5622  sotr2  5625  isso2i  5628  sotr3  5632  sotri2  6140  sotri3  6141  somin1  6144  somincom  6145  ordtri2  6410  ordtr3  6420  ordintdif  6425  ord0eln0  6430  soisoi  7339  weniso  7365  ordunisuc2  7853  limsssuc  7859  nlimon  7860  tfrlem15  8421  oawordeulem  8583  nnawordex  8666  onomeneqOLD  9266  fimaxg  9327  suplub2  9500  fiming  9537  wemapsolem  9589  cantnflem1  9728  rankval3b  9865  cardsdomel  10013  harsdom  10034  isfin1-2  10424  fin1a2lem7  10445  suplem2pr  11092  xrltnle  11327  ltnle  11339  leloe  11346  xrlttri  13167  xrleloe  13172  xrrebnd  13196  supxrbnd2  13350  supxrbnd  13356  om2uzf1oi  13968  rabssnn0fi  14001  cnpart  15240  bits0e  16424  bitsmod  16431  bitsinv1lem  16436  sadcaddlem  16452  trfil2  23874  xrsxmet  24808  metdsge  24848  ovolunlem1a  25508  ovolunlem1  25509  itg2seq  25755  noetasuplem4  27758  noetainflem4  27762  sltnle  27775  sleloe  27776  toslublem  32830  tosglblem  32832  isarchi2  33027  gsumesum  33848  sgnneg  34330  elfuns  35687  finminlem  35978  bj-bibibi  36239  itg2addnclem  37320  heiborlem10  37469  aks4d1p8  41734  cantnfresb  42927  naddwordnexlem4  43005  ontric3g  43126  or3or  43627  ntrclselnel2  43662  clsneifv3  43714  islininds2  47804