Theorem alcomw

Description: Weak version of alcom and biconditional form of alcomimw . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024)

	Ref	Expression
Hypotheses	alcomw.1	|- ( x = w -> ( ph <-> ps ) )
	alcomw.2	|- ( y = z -> ( ph <-> ch ) )
Assertion	alcomw	|- ( A. x A. y ph <-> A. y A. x ph )

Proof

Step	Hyp	Ref	Expression
1		alcomw.1	|- ( x = w -> ( ph <-> ps ) )
2		alcomw.2	|- ( y = z -> ( ph <-> ch ) )
3	2	alcomimw	|- ( A. x A. y ph -> A. y A. x ph )
4	1	alcomimw	|- ( A. y A. x ph -> A. x A. y ph )
5	3 4	impbii	|- ( A. x A. y ph <-> A. y A. x ph )