Theorem sylnibr 672

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 131	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 671	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2459  nssr  3207  difdif  3252  unssin  3366  inssun  3367  undif3ss  3388  ssdif0im  3478  dcun  3524  prneimg  3759  iundif2ss  3936  nssssr  4205  pofun  4295  frirrg  4333  regexmidlem1  4515  dcdifsnid  6480  unfidisj  6895  fidcenumlemrks  6926  difinfsn  7073  pw1nel3  7195  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemfl  7524  mulnqprlemfu  7525  cauappcvgprlemladdru  7605  caucvgprprlemaddq  7657  fzpreddisj  10014  fprodntrivap  11534  pw2dvdslemn  12106  isnsgrp  12634  ivthinclemdisj  13371  pwtrufal  13990  pw1nct  13996  nninfsellemsuc  14005