This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ x ∀ y φ ↔ ∀ y ∀ x φ

Proof

Step Hyp Ref Expression
1 alcomw.1 ⊢ x = w → φ ↔ ψ
2 alcomw.2 ⊢ y = z → φ ↔ χ
3 2 alcomimw ⊢ ∀ x ∀ y φ → ∀ y ∀ x φ
4 1 alcomimw ⊢ ∀ y ∀ x φ → ∀ x ∀ y φ
5 3 4 impbii ⊢ ∀ x ∀ y φ ↔ ∀ y ∀ x φ