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

Metamath Proof Explorer

Theorem mpnanrd

Description: Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 mpnanrd.1 ⊢ φ → ψ
2 mpnanrd.2 ⊢ φ → ¬ ψ ∧ χ
3 imnan ⊢ ψ → ¬ χ ↔ ¬ ψ ∧ χ
4 2 3 sylibr ⊢ φ → ψ → ¬ χ
5 1 4 mpd ⊢ φ → ¬ χ