Theorem 19.32

Theorem 19.32 of [Margaris] p. 90. See 19.32v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypothesis
19.32.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \forall x \, (\varphi \vee \psi) \leftrightarrow \varphi \vee \forall x \, \psi \)
Proof
19.32.1
nfn _
l2
19.21 _
\( \vdash \forall x \, (\neg \varphi \rightarrow \psi) \leftrightarrow \neg \varphi \rightarrow \forall x \, \psi \)
df-or
l4
albii _
\( \vdash \forall x \, (\varphi \vee \psi) \leftrightarrow \forall x \, (\neg \varphi \rightarrow \psi) \)
df-or
\( \vdash \varphi \vee \forall x \, \psi \leftrightarrow \neg \varphi \rightarrow \forall x \, \psi \)
3bitr4i l2 l4 _