Theorem sylnibr 666

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 131	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 665	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2425  nssr  3152  difdif  3196  unssin  3310  inssun  3311  undif3ss  3332  ssdif0im  3422  dcun  3468  prneimg  3696  iundif2ss  3873  nssssr  4139  pofun  4229  frirrg  4267  regexmidlem1  4443  dcdifsnid  6393  unfidisj  6803  fidcenumlemrks  6834  difinfsn  6978  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemfl  7376  mulnqprlemfu  7377  cauappcvgprlemladdru  7457  caucvgprprlemaddq  7509  fzpreddisj  9844  pw2dvdslemn  11832  ivthinclemdisj  12776  pwtrufal  13181  nninfsellemsuc  13197