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  5560  sotrieq  5561  sotr2  5564  isso2i  5567  sotr3  5571  sotri2  6084  sotri3  6085  somin1  6088  somincom  6089  ordtri2  6350  ordtr3  6361  ordintdif  6366  ord0eln0  6371  soisoi  7272  weniso  7298  ordunisuc2  7784  limsssuc  7790  nlimon  7791  tfrlem15  8321  oawordeulem  8479  nnawordex  8563  fimaxg  9185  suplub2  9362  fiming  9401  wemapsolem  9453  cantnflem1  9596  rankval3b  9736  cardsdomel  9884  harsdom  9905  isfin1-2  10293  fin1a2lem7  10314  suplem2pr  10962  xrltnle  11197  ltnle  11210  leloe  11217  xrlttri  13051  xrleloe  13056  xrrebnd  13081  supxrbnd2  13235  supxrbnd  13241  om2uzf1oi  13874  rabssnn0fi  13907  cnpart  15161  bits0e  16354  bitsmod  16361  bitsinv1lem  16366  sadcaddlem  16382  trfil2  23829  xrsxmet  24752  metdsge  24792  ovolunlem1a  25451  ovolunlem1  25452  itg2seq  25697  noetasuplem4  27702  noetainflem4  27706  sltnle  27719  sleloe  27720  sgnneg  32863  toslublem  33003  tosglblem  33005  isarchi2  33216  gsumesum  34165  elfuns  36056  finminlem  36461  bj-bibibi  36729  itg2addnclem  37811  heiborlem10  37960  aks4d1p8  42280  cantnfresb  43508  naddwordnexlem4  43585  ontric3g  43705  or3or  44206  ntrclselnel2  44241  clsneifv3  44293  islininds2  48672  resinsnlem  49058