Theorem alcom 715

Description: Theorem 19.5 of [Margaris] p. 89.

Assertion

Ref	Expression
alcom	⊢ (∀x∀yφ ↔ ∀y∀xφ)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 676	. 2 ⊢ (∀x∀yφ → ∀y∀xφ)
2		ax-7 676	. 2 ⊢ (∀y∀xφ → ∀x∀yφ)
3	1, 2	impbi 139	1 ⊢ (∀x∀yφ ↔ ∀y∀xφ)

Syntax hints:   ↔ wb 127  ∀wal 672

This theorem is referenced by:  sbcom 916  sbcom2 992  sbal2 1005  2eu4 1070  ralcom 1312  unissb 1941  dfiin2 2015  iunss 2017  ssiin 2024  dftr5 2044  cotr 2625  cnvsym 2626  dffun2 2674  f1fv 2916  aceq1 3552

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-7 676

This theorem depends on definitions:  df-bi 128

metamath.org