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  5564  sotrieq  5565  sotr2  5568  isso2i  5571  sotr3  5575  sotri2  6073  sotri3  6074  somin1  6077  somincom  6078  ordtri2  6341  ordtr3  6351  ordintdif  6355  ord0eln0  6360  soisoi  7259  weniso  7285  ordunisuc2  7762  limsssuc  7768  nlimon  7769  tfrlem15  8297  oawordeulem  8460  nnawordex  8543  onomeneqOLD  9098  fimaxg  9159  suplub2  9322  fiming  9359  wemapsolem  9411  cantnflem1  9550  rankval3b  9687  cardsdomel  9835  harsdom  9856  isfin1-2  10246  fin1a2lem7  10267  suplem2pr  10914  xrltnle  11147  ltnle  11159  leloe  11166  xrlttri  12978  xrleloe  12983  xrrebnd  13007  supxrbnd2  13161  supxrbnd  13167  om2uzf1oi  13778  rabssnn0fi  13811  cnpart  15050  bits0e  16235  bitsmod  16242  bitsinv1lem  16247  sadcaddlem  16263  trfil2  23143  xrsxmet  24077  metdsge  24117  ovolunlem1a  24765  ovolunlem1  24766  itg2seq  25012  noetasuplem4  26989  noetainflem4  26993  sltnle  27006  sleloe  27007  toslublem  31535  tosglblem  31537  isarchi2  31724  gsumesum  32323  sgnneg  32805  elfuns  34354  finminlem  34644  bj-bibibi  34905  itg2addnclem  35984  heiborlem10  36134  aks4d1p8  40400  ontric3g  41503  or3or  42004  ntrclselnel2  42041  clsneifv3  42093  islininds2  46243