Metamath Proof Explorer


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φψ
alcomw.2 y=zφχ
Assertion alcomw xyφyxφ

Proof

Step Hyp Ref Expression
1 alcomw.1 x=wφψ
2 alcomw.2 y=zφχ
3 2 alcomimw xyφyxφ
4 1 alcomimw yxφxyφ
5 3 4 impbii xyφyxφ