Theorem con2bid 354

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

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

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 207

This theorem is referenced by:  con1bid  355  sotric  5576  sotrieq  5577  sotr2  5580  isso2i  5583  sotr3  5587  sotri2  6102  sotri3  6103  somin1  6106  somincom  6107  ordtri2  6367  ordtr3  6378  ordintdif  6383  ord0eln0  6388  soisoi  7303  weniso  7329  ordunisuc2  7820  limsssuc  7826  nlimon  7827  tfrlem15  8360  oawordeulem  8518  nnawordex  8601  fimaxg  9234  suplub2  9412  fiming  9451  wemapsolem  9503  cantnflem1  9642  rankval3b  9779  cardsdomel  9927  harsdom  9948  isfin1-2  10338  fin1a2lem7  10359  suplem2pr  11006  xrltnle  11241  ltnle  11253  leloe  11260  xrlttri  13099  xrleloe  13104  xrrebnd  13128  supxrbnd2  13282  supxrbnd  13288  om2uzf1oi  13918  rabssnn0fi  13951  cnpart  15206  bits0e  16399  bitsmod  16406  bitsinv1lem  16411  sadcaddlem  16427  trfil2  23774  xrsxmet  24698  metdsge  24738  ovolunlem1a  25397  ovolunlem1  25398  itg2seq  25643  noetasuplem4  27648  noetainflem4  27652  sltnle  27665  sleloe  27666  sgnneg  32758  toslublem  32898  tosglblem  32900  isarchi2  33139  gsumesum  34049  elfuns  35903  finminlem  36306  bj-bibibi  36574  itg2addnclem  37665  heiborlem10  37814  aks4d1p8  42075  cantnfresb  43313  naddwordnexlem4  43390  ontric3g  43511  or3or  44012  ntrclselnel2  44047  clsneifv3  44099  islininds2  48470  resinsnlem  48856