Theorem sylnibr 688

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnibr.1	⊢ (𝜑 → ¬ 𝜓)
sylnibr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylnibr	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem sylnibr

Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		sylnibr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 132	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 687	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2539  nssr  3308  difdif  3354  unssin  3470  inssun  3471  undif3ss  3492  ssdif0im  3588  dcun  3634  prneimg  3894  iundif2ss  4073  nssssr  4357  pofun  4452  frirrg  4490  regexmidlem1  4675  dcdifsnid  6767  elssdc  7199  unfidisj  7219  fidcenumlemrks  7260  difinfsn  7430  pw1nel3  7580  addnqprlemfl  7916  addnqprlemfu  7917  mulnqprlemfl  7932  mulnqprlemfu  7933  cauappcvgprlemladdru  8013  caucvgprprlemaddq  8065  fzpreddisj  10456  ccatalpha  11359  fprodntrivap  12329  pw2dvdslemn  12921  isnsgrp  13698  ivthinclemdisj  15664  dvply1  15789  lgseisenlem1  16103  lgsquadlem3  16112  structiedg0val  16195  umgr2edg1  16364  umgr2edgneu  16367  trlsegvdegfi  16622  pwtrufal  16941  pw1nct  16947  nninfsellemsuc  16960