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  5596  sotrieq  5597  sotr2  5600  isso2i  5603  sotr3  5607  sotri2  6123  sotri3  6124  somin1  6127  somincom  6128  ordtri2  6392  ordtr3  6403  ordintdif  6408  ord0eln0  6413  soisoi  7326  weniso  7352  ordunisuc2  7844  limsssuc  7850  nlimon  7851  tfrlem15  8411  oawordeulem  8571  nnawordex  8654  onomeneqOLD  9243  fimaxg  9300  suplub2  9478  fiming  9517  wemapsolem  9569  cantnflem1  9708  rankval3b  9845  cardsdomel  9993  harsdom  10014  isfin1-2  10404  fin1a2lem7  10425  suplem2pr  11072  xrltnle  11307  ltnle  11319  leloe  11326  xrlttri  13160  xrleloe  13165  xrrebnd  13189  supxrbnd2  13343  supxrbnd  13349  om2uzf1oi  13976  rabssnn0fi  14009  cnpart  15264  bits0e  16453  bitsmod  16460  bitsinv1lem  16465  sadcaddlem  16481  trfil2  23830  xrsxmet  24754  metdsge  24794  ovolunlem1a  25454  ovolunlem1  25455  itg2seq  25700  noetasuplem4  27705  noetainflem4  27709  sltnle  27722  sleloe  27723  sgnneg  32817  toslublem  32957  tosglblem  32959  isarchi2  33188  gsumesum  34095  elfuns  35938  finminlem  36341  bj-bibibi  36609  itg2addnclem  37700  heiborlem10  37849  aks4d1p8  42105  cantnfresb  43315  naddwordnexlem4  43392  ontric3g  43513  or3or  44014  ntrclselnel2  44049  clsneifv3  44101  islininds2  48427  resinsnlem  48813