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 ( 𝑥 = 𝑤 → ( 𝜑𝜓 ) )
alcomw.2 ( 𝑦 = 𝑧 → ( 𝜑𝜒 ) )
Assertion alcomw ( ∀ 𝑥𝑦 𝜑 ↔ ∀ 𝑦𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 alcomw.1 ( 𝑥 = 𝑤 → ( 𝜑𝜓 ) )
2 alcomw.2 ( 𝑦 = 𝑧 → ( 𝜑𝜒 ) )
3 2 alcomiw ( ∀ 𝑥𝑦 𝜑 → ∀ 𝑦𝑥 𝜑 )
4 1 alcomiw ( ∀ 𝑦𝑥 𝜑 → ∀ 𝑥𝑦 𝜑 )
5 3 4 impbii ( ∀ 𝑥𝑦 𝜑 ↔ ∀ 𝑦𝑥 𝜑 )