Theorem sylnibr 678

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 677	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2486  nssr  3243  difdif  3288  unssin  3402  inssun  3403  undif3ss  3424  ssdif0im  3515  dcun  3560  prneimg  3804  iundif2ss  3982  nssssr  4255  pofun  4347  frirrg  4385  regexmidlem1  4569  dcdifsnid  6562  unfidisj  6983  fidcenumlemrks  7019  difinfsn  7166  pw1nel3  7298  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemfl  7642  mulnqprlemfu  7643  cauappcvgprlemladdru  7723  caucvgprprlemaddq  7775  fzpreddisj  10146  fprodntrivap  11749  pw2dvdslemn  12333  isnsgrp  13049  ivthinclemdisj  14876  dvply1  15001  lgseisenlem1  15311  lgsquadlem3  15320  pwtrufal  15642  pw1nct  15647  nninfsellemsuc  15656