Theorem 19.31

Theorem 19.31 of [Margaris] p. 90. See 19.31v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.)

Hypothesis
19.31.1
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \forall x \, (\varphi \vee \psi) \leftrightarrow \forall x \, \varphi \vee \psi \)
Proof
19.31.1
l1
19.32 _
\( \vdash \forall x \, (\psi \vee \varphi) \leftrightarrow \psi \vee \forall x \, \varphi \)
orcom
l3
albii _
\( \vdash \forall x \, (\varphi \vee \psi) \leftrightarrow \forall x \, (\psi \vee \varphi) \)
orcom
\( \vdash \forall x \, \varphi \vee \psi \leftrightarrow \psi \vee \forall x \, \varphi \)
3bitr4i l1 l3 _