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 -> ( ph <-> ps ) )
Assertion	alcomiwOLD	|- ( A. x A. y ph -> A. y A. x ph )

Proof

Step	Hyp	Ref	Expression
1		alcomiw.1	|- ( y = z -> ( ph <-> ps ) )
2	1	biimpd	|- ( y = z -> ( ph -> ps ) )
3	2	cbvalivw	|- ( A. y ph -> A. z ps )
4	3	alimi	|- ( A. x A. y ph -> A. x A. z ps )
5		ax-5	|- ( A. x A. z ps -> A. y A. x A. z ps )
6	1	biimprd	|- ( y = z -> ( ps -> ph ) )
7	6	equcoms	|- ( z = y -> ( ps -> ph ) )
8	7	spimvw	|- ( A. z ps -> ph )
9	8	2alimi	|- ( A. y A. x A. z ps -> A. y A. x ph )
10	4 5 9	3syl	|- ( A. x A. y ph -> A. y A. x ph )