Metamath Proof Explorer

Theorem pm3.48

Description: Theorem *3.48 of WhiteheadRussell p. 114. (Contributed by NM, 28-Jan-1997)

Ref Expression
Assertion pm3.48 ⊢ φ → ψ ∧ χ → θ → φ ∨ χ → ψ ∨ θ

Proof

Step Hyp Ref Expression
1 orc ⊢ ψ → ψ ∨ θ
2 1 imim2i ⊢ φ → ψ → φ → ψ ∨ θ
3 olc ⊢ θ → ψ ∨ θ
4 3 imim2i ⊢ χ → θ → χ → ψ ∨ θ
5 2 4 jaao ⊢ φ → ψ ∧ χ → θ → φ ∨ χ → ψ ∨ θ