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  2483  nssr  3240  difdif  3285  unssin  3399  inssun  3400  undif3ss  3421  ssdif0im  3512  dcun  3557  prneimg  3801  iundif2ss  3979  nssssr  4252  pofun  4344  frirrg  4382  regexmidlem1  4566  dcdifsnid  6559  unfidisj  6980  fidcenumlemrks  7014  difinfsn  7161  pw1nel3  7293  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemfl  7637  mulnqprlemfu  7638  cauappcvgprlemladdru  7718  caucvgprprlemaddq  7770  fzpreddisj  10140  fprodntrivap  11730  pw2dvdslemn  12306  isnsgrp  12992  ivthinclemdisj  14819  dvply1  14943  lgseisenlem1  15227  lgsquadlem3  15236  pwtrufal  15558  pw1nct  15563  nninfsellemsuc  15572