Theorem jaob

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.)

Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \)
Proof
l0
pm2.67-2
olc
imim1i _
l3
jca l0 _
pm3.44
impbii l3 _