Metamath Proof Explorer

Theorem orel

Description: An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypotheses orel.1 ⊢ ψ ∧ η → θ
orel.2 ⊢ χ ∧ ρ → θ
orel.3 ⊢ φ → ψ ∨ χ
Assertion orel ⊢ φ ∧ η ∧ ρ → θ

Proof

Step Hyp Ref Expression
1 orel.1 ⊢ ψ ∧ η → θ
2 orel.2 ⊢ χ ∧ ρ → θ
3 orel.3 ⊢ φ → ψ ∨ χ
4 simprl ⊢ φ ∧ η ∧ ρ → η
5 1 ancoms ⊢ η ∧ ψ → θ
6 4 5 sylan ⊢ φ ∧ η ∧ ρ ∧ ψ → θ
7 simprr ⊢ φ ∧ η ∧ ρ → ρ
8 2 ancoms ⊢ ρ ∧ χ → θ
9 7 8 sylan ⊢ φ ∧ η ∧ ρ ∧ χ → θ
10 3 adantr ⊢ φ ∧ η ∧ ρ → ψ ∨ χ
11 6 9 10 mpjaodan ⊢ φ ∧ η ∧ ρ → θ