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

Metamath Proof Explorer

Theorem nsyl5

Description: A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024)

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

Proof

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