Theorem sylnibr 684

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 683	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  2522  nssr  3288  difdif  3334  unssin  3448  inssun  3449  undif3ss  3470  ssdif0im  3561  dcun  3606  prneimg  3862  iundif2ss  4041  nssssr  4320  pofun  4415  frirrg  4453  regexmidlem1  4637  dcdifsnid  6715  elssdc  7137  unfidisj  7157  fidcenumlemrks  7195  difinfsn  7342  pw1nel3  7492  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  cauappcvgprlemladdru  7919  caucvgprprlemaddq  7971  fzpreddisj  10351  ccatalpha  11239  fprodntrivap  12208  pw2dvdslemn  12800  isnsgrp  13552  ivthinclemdisj  15434  dvply1  15559  lgseisenlem1  15872  lgsquadlem3  15881  structiedg0val  15964  umgr2edg1  16133  umgr2edgneu  16136  trlsegvdegfi  16391  pwtrufal  16702  pw1nct  16708  nninfsellemsuc  16721