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 φ ψ
Assertion alcomiwOLD x y φ y x φ


Step Hyp Ref Expression
1 alcomiw.1 y = z φ ψ
2 1 biimpd y = z φ ψ
3 2 cbvalivw y φ z ψ
4 3 alimi x y φ x z ψ
5 ax-5 x z ψ y x z ψ
6 1 biimprd y = z ψ φ
7 6 equcoms z = y ψ φ
8 7 spimvw z ψ φ
9 8 2alimi y x z ψ y x φ
10 4 5 9 3syl x y φ y x φ