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

Proof

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