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

Metamath Proof Explorer

Theorem pm3.2ni

Description: Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995)

Ref Expression
Hypotheses pm3.2ni.1 ⊢ ¬ 𝜑
pm3.2ni.2 ⊢ ¬ 𝜓
Assertion pm3.2ni ¬ ( 𝜑 ∨ 𝜓 )

Proof

Step Hyp Ref Expression
1 pm3.2ni.1 ⊢ ¬ 𝜑
2 pm3.2ni.2 ⊢ ¬ 𝜓
3 id ⊢ ( 𝜑 → 𝜑 )
4 2 pm2.21i ⊢ ( 𝜓 → 𝜑 )
5 3 4 jaoi ⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜑 )
6 1 5 mto ⊢ ¬ ( 𝜑 ∨ 𝜓 )