# Metamath Proof Explorer

## Theorem alcomiwOLD

Description: Obsolete version of alcomiw as of 28-Dec-2023. (Contributed by NM, 10-Apr-2017) (Proof shortened by Wolf Lammen, 12-Jul-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis alcomiw.1 ${⊢}{y}={z}\to \left({\phi }↔{\psi }\right)$
Assertion alcomiwOLD ${⊢}\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 biimpd ${⊢}{y}={z}\to \left({\phi }\to {\psi }\right)$
3 2 cbvalivw ${⊢}\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 }$