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

Proof

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