Theorem sylnibr 681

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 680	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2519  nssr  3285  difdif  3330  unssin  3444  inssun  3445  undif3ss  3466  ssdif0im  3557  dcun  3602  prneimg  3855  iundif2ss  4034  nssssr  4312  pofun  4407  frirrg  4445  regexmidlem1  4629  dcdifsnid  6667  elssdc  7087  unfidisj  7107  fidcenumlemrks  7143  difinfsn  7290  pw1nel3  7439  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprlemfl  7785  mulnqprlemfu  7786  cauappcvgprlemladdru  7866  caucvgprprlemaddq  7918  fzpreddisj  10296  ccatalpha  11180  fprodntrivap  12135  pw2dvdslemn  12727  isnsgrp  13479  ivthinclemdisj  15354  dvply1  15479  lgseisenlem1  15789  lgsquadlem3  15798  structiedg0val  15881  umgr2edg1  16048  umgr2edgneu  16051  pwtrufal  16534  pw1nct  16540  nninfsellemsuc  16550