Theorem alcomw

Weak version of alcom and biconditional form of alcomimw. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)

Hypotheses
alcomw.1
\( \vdash x = w \rightarrow (\varphi \leftrightarrow \psi) \)
alcomw.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \leftrightarrow \forall y \, \forall x \, \varphi \)
Proof
alcomw.2
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \chi) \)
l1
alcomimw _
alcomw.1
\( \vdash x = w \rightarrow (\varphi \leftrightarrow \psi) \)
alcomimw _
impbii l1 _