Metamath Proof Explorer


Theorem pm3.44

Description: Theorem *3.44 of WhiteheadRussell p. 113. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 3-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 id ⊢ ψ → φ → ψ → φ
2 id ⊢ χ → φ → χ → φ
3 1 2 jaao ⊢ ψ → φ ∧ χ → φ → ψ ∨ χ → φ