Theorem sylnibr 679

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 678	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  2496  nssr  3257  difdif  3302  unssin  3416  inssun  3417  undif3ss  3438  ssdif0im  3529  dcun  3574  prneimg  3821  iundif2ss  3999  nssssr  4274  pofun  4367  frirrg  4405  regexmidlem1  4589  dcdifsnid  6603  unfidisj  7034  fidcenumlemrks  7070  difinfsn  7217  pw1nel3  7362  addnqprlemfl  7692  addnqprlemfu  7693  mulnqprlemfl  7708  mulnqprlemfu  7709  cauappcvgprlemladdru  7789  caucvgprprlemaddq  7841  fzpreddisj  10213  fprodntrivap  11970  pw2dvdslemn  12562  isnsgrp  13313  ivthinclemdisj  15187  dvply1  15312  lgseisenlem1  15622  lgsquadlem3  15631  structiedg0val  15714  pwtrufal  16075  pw1nct  16081  nninfsellemsuc  16090