Theorem con2bid 355

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 354	. 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  356  sotric  5617  sotrieq  5618  sotr2  5621  isso2i  5624  sotr3  5628  sotri2  6131  sotri3  6132  somin1  6135  somincom  6136  ordtri2  6400  ordtr3  6410  ordintdif  6415  ord0eln0  6420  soisoi  7325  weniso  7351  ordunisuc2  7833  limsssuc  7839  nlimon  7840  tfrlem15  8392  oawordeulem  8554  nnawordex  8637  onomeneqOLD  9229  fimaxg  9290  suplub2  9456  fiming  9493  wemapsolem  9545  cantnflem1  9684  rankval3b  9821  cardsdomel  9969  harsdom  9990  isfin1-2  10380  fin1a2lem7  10401  suplem2pr  11048  xrltnle  11281  ltnle  11293  leloe  11300  xrlttri  13118  xrleloe  13123  xrrebnd  13147  supxrbnd2  13301  supxrbnd  13307  om2uzf1oi  13918  rabssnn0fi  13951  cnpart  15187  bits0e  16370  bitsmod  16377  bitsinv1lem  16382  sadcaddlem  16398  trfil2  23391  xrsxmet  24325  metdsge  24365  ovolunlem1a  25013  ovolunlem1  25014  itg2seq  25260  noetasuplem4  27239  noetainflem4  27243  sltnle  27256  sleloe  27257  toslublem  32142  tosglblem  32144  isarchi2  32331  gsumesum  33057  sgnneg  33539  elfuns  34887  finminlem  35203  bj-bibibi  35464  itg2addnclem  36539  heiborlem10  36688  aks4d1p8  40952  cantnfresb  42074  naddwordnexlem4  42152  ontric3g  42273  or3or  42774  ntrclselnel2  42809  clsneifv3  42861  islininds2  47165