# Metamath Proof Explorer

## Theorem alcomiw

Description: Weak version of alcom . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017) (Proof shortened by Wolf Lammen, 28-Dec-2023)

Ref Expression
Hypothesis alcomiw.1 ${⊢}{y}={z}\to \left({\phi }↔{\psi }\right)$
Assertion alcomiw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 alcomiw.1 ${⊢}{y}={z}\to \left({\phi }↔{\psi }\right)$
2 1 cbvalvw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
3 2 biimpi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
4 3 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
5 ax-5 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
6 1 biimprd ${⊢}{y}={z}\to \left({\psi }\to {\phi }\right)$
7 6 equcoms ${⊢}{z}={y}\to \left({\psi }\to {\phi }\right)$
8 7 spimvw ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }\to {\phi }$
9 8 2alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
10 4 5 9 3syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$