Theorem sylnibr 677

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 676	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2466  nssr  3217  difdif  3262  unssin  3376  inssun  3377  undif3ss  3398  ssdif0im  3489  dcun  3535  prneimg  3776  iundif2ss  3954  nssssr  4224  pofun  4314  frirrg  4352  regexmidlem1  4534  dcdifsnid  6507  unfidisj  6923  fidcenumlemrks  6954  difinfsn  7101  pw1nel3  7232  addnqprlemfl  7560  addnqprlemfu  7561  mulnqprlemfl  7576  mulnqprlemfu  7577  cauappcvgprlemladdru  7657  caucvgprprlemaddq  7709  fzpreddisj  10073  fprodntrivap  11594  pw2dvdslemn  12167  isnsgrp  12817  ivthinclemdisj  14203  lgseisenlem1  14535  pwtrufal  14832  pw1nct  14837  nninfsellemsuc  14846