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  2486  nssr  3244  difdif  3289  unssin  3403  inssun  3404  undif3ss  3425  ssdif0im  3516  dcun  3561  prneimg  3805  iundif2ss  3983  nssssr  4256  pofun  4348  frirrg  4386  regexmidlem1  4570  dcdifsnid  6571  unfidisj  6992  fidcenumlemrks  7028  difinfsn  7175  pw1nel3  7316  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemfl  7661  mulnqprlemfu  7662  cauappcvgprlemladdru  7742  caucvgprprlemaddq  7794  fzpreddisj  10165  fprodntrivap  11768  pw2dvdslemn  12360  isnsgrp  13110  ivthinclemdisj  14984  dvply1  15109  lgseisenlem1  15419  lgsquadlem3  15428  pwtrufal  15752  pw1nct  15758  nninfsellemsuc  15767