Theorem alcomimw
Weak version of [ax-11]. See alcomw for the biconditional form.
Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.)
(Proof shortened by Wolf Lammen, 28-Dec-2023.)
Hypothesis
alcomimw.1
\( \vdash y = z \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
Proof
alcomimw.1
cbvalvw _
biimpi _
l3
alimi _
\( \vdash \forall x \, \forall y \, \varphi \rightarrow \forall x \, \forall z \, \psi \)
l4
ax-5
\( \vdash \forall x \, \forall z \, \psi \rightarrow \forall y \, \forall x \, \forall z \, \psi \)
alcomimw.1
biimprd _
equcoms _
\( \vdash z = y \rightarrow \psi \rightarrow \varphi \)
spimvw _
2alimi _
\( \vdash \forall y \, \forall x \, \forall z \, \psi \rightarrow \forall y \, \forall x \, \varphi \)
3syl l3 l4 _