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

Metamath Proof Explorer

Theorem alcomimw

Description: Weak version of ax-11 . See alcomw for the biconditional form. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017) (Proof shortened by Wolf Lammen, 28-Dec-2023)

Ref Expression
Hypothesis alcomimw.1 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
Assertion alcomimw ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 alcomimw.1 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2 1 cbvalvw ⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑧 𝜓 )
3 2 biimpi ⊢ ( ∀ 𝑦 𝜑 → ∀ 𝑧 𝜓 )
4 3 alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑧 𝜓 )
5 ax-5 ⊢ ( ∀ 𝑥 ∀ 𝑧 𝜓 → ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜓 )
6 1 biimprd ⊢ ( 𝑦 = 𝑧 → ( 𝜓 → 𝜑 ) )
7 6 equcoms ⊢ ( 𝑧 = 𝑦 → ( 𝜓 → 𝜑 ) )
8 7 spimvw ⊢ ( ∀ 𝑧 𝜓 → 𝜑 )
9 8 2alimi ⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜓 → ∀ 𝑦 ∀ 𝑥 𝜑 )
10 4 5 9 3syl ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )