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  3284  difdif  3329  unssin  3443  inssun  3444  undif3ss  3465  ssdif0im  3556  dcun  3601  prneimg  3851  iundif2ss  4030  nssssr  4307  pofun  4402  frirrg  4440  regexmidlem1  4624  dcdifsnid  6648  unfidisj  7080  fidcenumlemrks  7116  difinfsn  7263  pw1nel3  7412  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemfl  7758  mulnqprlemfu  7759  cauappcvgprlemladdru  7839  caucvgprprlemaddq  7891  fzpreddisj  10263  fprodntrivap  12090  pw2dvdslemn  12682  isnsgrp  13434  ivthinclemdisj  15308  dvply1  15433  lgseisenlem1  15743  lgsquadlem3  15752  structiedg0val  15835  umgr2edg1  16001  umgr2edgneu  16004  pwtrufal  16322  pw1nct  16328  nninfsellemsuc  16337