Theorem sylnibr 683

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 682	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2521  nssr  3287  difdif  3332  unssin  3446  inssun  3447  undif3ss  3468  ssdif0im  3559  dcun  3604  prneimg  3857  iundif2ss  4036  nssssr  4314  pofun  4409  frirrg  4447  regexmidlem1  4631  dcdifsnid  6671  elssdc  7093  unfidisj  7113  fidcenumlemrks  7151  difinfsn  7298  pw1nel3  7448  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemfl  7794  mulnqprlemfu  7795  cauappcvgprlemladdru  7875  caucvgprprlemaddq  7927  fzpreddisj  10305  ccatalpha  11189  fprodntrivap  12144  pw2dvdslemn  12736  isnsgrp  13488  ivthinclemdisj  15363  dvply1  15488  lgseisenlem1  15798  lgsquadlem3  15807  structiedg0val  15890  umgr2edg1  16059  umgr2edgneu  16062  pwtrufal  16598  pw1nct  16604  nninfsellemsuc  16614