Theorem nsyl 102

Description: A negated syllogism inference.

Hypotheses

Ref	Expression
nsyl.1	⊢ (φ → ¬ ψ)
nsyl.2	⊢ (χ → ψ)

Assertion

Ref	Expression
nsyl	⊢ (φ → ¬ χ)

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. 2 ⊢ (φ → ¬ ψ)
2		nsyl.2	. . 3 ⊢ (χ → ψ)
3	2	con3i 90	. 2 ⊢ (¬ ψ → ¬ χ)
4	1, 3	syl 12	1 ⊢ (φ → ¬ χ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.65i 116  msca 508  disjsn 1836  dfwe2 2187  ordnbtwn 2316  nlimsuc 2363  funun 2700  tfrlem13 2961  oprssdm 3056  php2 3410  inf5 3472  cardaleph 3690  axrepnd 3740  suplem2pr 3956  elnnz 4572  elnnz1 4581  ruclem28 4912

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org