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

Metamath Proof Explorer

Theorem pm2.61dda

Description: Elimination of two antecedents. (Contributed by NM, 9-Jul-2013)

Ref Expression
Hypotheses pm2.61dda.1 ⊢ φ ∧ ¬ ψ → θ
pm2.61dda.2 ⊢ φ ∧ ¬ χ → θ
pm2.61dda.3 ⊢ φ ∧ ψ ∧ χ → θ
Assertion pm2.61dda ⊢ φ → θ

Proof

Step Hyp Ref Expression
1 pm2.61dda.1 ⊢ φ ∧ ¬ ψ → θ
2 pm2.61dda.2 ⊢ φ ∧ ¬ χ → θ
3 pm2.61dda.3 ⊢ φ ∧ ψ ∧ χ → θ
4 3 anassrs ⊢ φ ∧ ψ ∧ χ → θ
5 2 adantlr ⊢ φ ∧ ψ ∧ ¬ χ → θ
6 4 5 pm2.61dan ⊢ φ ∧ ψ → θ
7 6 1 pm2.61dan ⊢ φ → θ