Theorem orim12dALT

Alternate proof of orim12d which does not depend on [df-an]. This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
orim12dALT.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
orim12dALT.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \theta \rightarrow \chi \vee \tau \)
Proof
l0
pm2.53
\( \vdash \psi \vee \theta \rightarrow \neg \psi \rightarrow \theta \)
orim12dALT.1
l2
con3d _
orim12dALT.2
l4
imim12d l2 _
\( \vdash \varphi \rightarrow (\neg \psi \rightarrow \theta) \rightarrow \neg \chi \rightarrow \tau \)
pm2.54
\( \vdash (\neg \chi \rightarrow \tau) \rightarrow \chi \vee \tau \)
syl56 l0 l4 _