Theorem aaan
Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993.)
Avoid [ax-10]. (Revised by GG, 21-Nov-2024.)
Hypotheses
aaan.1
\( \vdash \Finv y \, \varphi \)
aaan.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \forall x \, \forall y \, (\varphi \wedge \psi) \leftrightarrow \forall x \, \varphi \wedge \forall y \, \psi \)
Proof
l0
19.26-2
\( \vdash \forall x \, \forall y \, (\varphi \wedge \psi) \leftrightarrow \forall x \, \forall y \, \varphi \wedge \forall x \, \forall y \, \psi \)
aaan.1
19.3 _
l3
albii _
l4
alcom
\( \vdash \forall x \, \forall y \, \psi \leftrightarrow \forall y \, \forall x \, \psi \)
aaan.2
19.3 _
albii _
\( \vdash \forall y \, \forall x \, \psi \leftrightarrow \forall y \, \psi \)
bitri l4 _
anbi12i l3 _
\( \vdash \forall x \, \forall y \, \varphi \wedge \forall x \, \forall y \, \psi \leftrightarrow \forall x \, \varphi \wedge \forall y \, \psi \)
bitri l0 _