Theorem sylnibr 634

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  rexnalim  2359  nssr  3057  difdif  3097  unssin  3203  inssun  3204  undif3ss  3225  ssdif0im  3308  prneimg  3566  iundif2ss  3743  nssssr  3977  pofun  4067  frirrg  4105  regexmidlem1  4276  nndifsnid  6103  fidifsnid  6356  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemfl  6765  mulnqprlemfu  6766  cauappcvgprlemladdru  6846  caucvgprprlemaddq  6898  fzpreddisj  9088  pw2dvdslemn  10543