Theorem sylnibr 681

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 680	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2519  nssr  3284  difdif  3329  unssin  3443  inssun  3444  undif3ss  3465  ssdif0im  3556  dcun  3601  prneimg  3852  iundif2ss  4031  nssssr  4308  pofun  4403  frirrg  4441  regexmidlem1  4625  dcdifsnid  6658  elssdc  7075  unfidisj  7095  fidcenumlemrks  7131  difinfsn  7278  pw1nel3  7427  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  cauappcvgprlemladdru  7854  caucvgprprlemaddq  7906  fzpreddisj  10279  ccatalpha  11161  fprodntrivap  12110  pw2dvdslemn  12702  isnsgrp  13454  ivthinclemdisj  15329  dvply1  15454  lgseisenlem1  15764  lgsquadlem3  15773  structiedg0val  15856  umgr2edg1  16022  umgr2edgneu  16025  pwtrufal  16422  pw1nct  16428  nninfsellemsuc  16438