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  2483  nssr  3239  difdif  3284  unssin  3398  inssun  3399  undif3ss  3420  ssdif0im  3511  dcun  3556  prneimg  3800  iundif2ss  3978  nssssr  4251  pofun  4343  frirrg  4381  regexmidlem1  4565  dcdifsnid  6557  unfidisj  6978  fidcenumlemrks  7012  difinfsn  7159  pw1nel3  7291  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemfl  7635  mulnqprlemfu  7636  cauappcvgprlemladdru  7716  caucvgprprlemaddq  7768  fzpreddisj  10137  fprodntrivap  11727  pw2dvdslemn  12303  isnsgrp  12989  ivthinclemdisj  14794  lgseisenlem1  15186  pwtrufal  15488  pw1nct  15493  nninfsellemsuc  15502