This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nsyl4

Description: A negated syllogism inference. (Contributed by NM, 15-Feb-1996)

Ref Expression
Hypotheses nsyl4.1 ⊢ φ → ψ
nsyl4.2 ⊢ ¬ φ → χ
Assertion nsyl4 ⊢ ¬ χ → ψ

Proof

Step Hyp Ref Expression
1 nsyl4.1 ⊢ φ → ψ
2 nsyl4.2 ⊢ ¬ φ → χ
3 2 con1i ⊢ ¬ χ → φ
4 3 1 syl ⊢ ¬ χ → ψ