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  6672  elssdc  7094  unfidisj  7114  fidcenumlemrks  7152  difinfsn  7299  pw1nel3  7449  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  cauappcvgprlemladdru  7876  caucvgprprlemaddq  7928  fzpreddisj  10306  ccatalpha  11194  fprodntrivap  12163  pw2dvdslemn  12755  isnsgrp  13507  ivthinclemdisj  15383  dvply1  15508  lgseisenlem1  15818  lgsquadlem3  15827  structiedg0val  15910  umgr2edg1  16079  umgr2edgneu  16082  trlsegvdegfi  16337  pwtrufal  16649  pw1nct  16655  nninfsellemsuc  16665