Theorem sylnibr 678

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 677	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2494  nssr  3252  difdif  3297  unssin  3411  inssun  3412  undif3ss  3433  ssdif0im  3524  dcun  3569  prneimg  3814  iundif2ss  3992  nssssr  4265  pofun  4358  frirrg  4396  regexmidlem1  4580  dcdifsnid  6589  unfidisj  7018  fidcenumlemrks  7054  difinfsn  7201  pw1nel3  7342  addnqprlemfl  7671  addnqprlemfu  7672  mulnqprlemfl  7687  mulnqprlemfu  7688  cauappcvgprlemladdru  7768  caucvgprprlemaddq  7820  fzpreddisj  10192  fprodntrivap  11837  pw2dvdslemn  12429  isnsgrp  13180  ivthinclemdisj  15054  dvply1  15179  lgseisenlem1  15489  lgsquadlem3  15498  structiedg0val  15579  pwtrufal  15867  pw1nct  15873  nninfsellemsuc  15882