Theorem sylnibr 602

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  rexnalim  2317  nssr  3003  difdif  3069  unssin  3176  inssun  3177  undif3ss  3198  ssdif0im  3286  prneimg  3545  iundif2ss  3722  nssssr  3958  pofun  4049  frirrg  4087  regexmidlem1  4258  nndifsnid  6080  fidifsnid  6332  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemfl  6673  mulnqprlemfu  6674  cauappcvgprlemladdru  6754  caucvgprprlemaddq  6806  fzpreddisj  8933