Theorem sylnibr 643

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 131	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 642	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2386  nssr  3107  difdif  3148  unssin  3262  inssun  3263  undif3ss  3284  ssdif0im  3374  dcun  3420  prneimg  3648  iundif2ss  3825  nssssr  4082  pofun  4172  frirrg  4210  regexmidlem1  4386  dcdifsnid  6330  unfidisj  6739  fidcenumlemrks  6769  difinfsn  6900  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemfl  7284  mulnqprlemfu  7285  cauappcvgprlemladdru  7365  caucvgprprlemaddq  7417  fzpreddisj  9692  pw2dvdslemn  11635  pwtrufal  12777  nninfsellemsuc  12792