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

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

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 210

This theorem is referenced by:  con1bid  358  sotric  5600  sotrieq  5601  sotr2  5604  isso2i  5607  sotr3  5611  sotri2  6130  sotri3  6131  somin1  6134  somincom  6135  ordtri2  6397  ordtr3  6408  ordintdif  6413  ord0eln0  6418  soisoi  7327  weniso  7353  ordunisuc2  7839  limsssuc  7845  nlimon  7846  tfrlem15  8378  oawordeulem  8538  nnawordex  8622  fimaxg  9246  suplub2  9420  fiming  9459  wemapsolem  9511  cantnflem1  9657  rankval3b  9797  cardsdomel  9959  harsdom  9980  isfin1-2  10368  fin1a2lem7  10389  suplem2pr  11037  xrltnle  11275  ltnle  11288  leloe  11295  xrlttri  13163  xrleloe  13168  xrrebnd  13193  supxrbnd2  13347  supxrbnd  13353  om2uzf1oi  13988  rabssnn0fi  14021  sgnneg  15136  cnpart  15290  bits0e  16486  bitsmod  16493  bitsinv1lem  16498  sadcaddlem  16514  trfil2  24012  xrsxmet  24935  metdsge  24975  ovolunlem1a  25623  ovolunlem1  25624  itg2seq  25869  noetasuplem4  27865  noetainflem4  27869  ltnles  27882  lesloe  27883  toslublem  33232  tosglblem  33234  isarchi2  33445  gsumesum  34393  elfuns  36303  finminlem  36717  bj-bibibi  37067  itg2addnclem  38209  heiborlem10  38358  aks4d1p8  42743  cantnfresb  43942  naddwordnexlem4  44019  ontric3g  44139  or3or  44640  ntrclselnel2  44675  clsneifv3  44727  islininds2  49148  resinsnlem  49533