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 ⊢ ( 𝜑 → ¬ 𝜒 )