Theorem sylnibr 667

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 666	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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2428  nssr  3162  difdif  3206  unssin  3320  inssun  3321  undif3ss  3342  ssdif0im  3432  dcun  3478  prneimg  3709  iundif2ss  3886  nssssr  4152  pofun  4242  frirrg  4280  regexmidlem1  4456  dcdifsnid  6408  unfidisj  6818  fidcenumlemrks  6849  difinfsn  6993  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemfl  7407  mulnqprlemfu  7408  cauappcvgprlemladdru  7488  caucvgprprlemaddq  7540  fzpreddisj  9882  pw2dvdslemn  11879  ivthinclemdisj  12826  pwtrufal  13365  pw1nct  13371  nninfsellemsuc  13383