Metamath Proof Explorer


Theorem alcomw

Description: Weak version of alcom and biconditional form of alcomiw . 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 alcomiw
 |-  ( A. x A. y ph -> A. y A. x ph )
4 1 alcomiw
 |-  ( A. y A. x ph -> A. x A. y ph )
5 3 4 impbii
 |-  ( A. x A. y ph <-> A. y A. x ph )