Metamath Proof Explorer

Theorem jaob

Description: Disjunction of antecedents. Compare Theorem *4.77 of WhiteheadRussell p. 121. (Contributed by NM, 30-May-1994) (Proof shortened by Wolf Lammen, 9-Dec-2012)

Ref Expression
Assertion jaob ⊢ φ ∨ χ → ψ ↔ φ → ψ ∧ χ → ψ

Proof

Step Hyp Ref Expression
1 pm2.67-2 ⊢ φ ∨ χ → ψ → φ → ψ
2 olc ⊢ χ → φ ∨ χ
3 2 imim1i ⊢ φ ∨ χ → ψ → χ → ψ
4 1 3 jca ⊢ φ ∨ χ → ψ → φ → ψ ∧ χ → ψ
5 pm3.44 ⊢ φ → ψ ∧ χ → ψ → φ ∨ χ → ψ
6 4 5 impbii ⊢ φ ∨ χ → ψ ↔ φ → ψ ∧ χ → ψ