Theorem alcom 1492

Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
alcom	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 1462	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-7 1462	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 126	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 105  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-7 1462

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1499  alrot4  1500  nfalt  1592  nfexd  1775  sbnf2  2000  sbcom2v  2004  sbalyz  2018  sbal1yz  2020  sbal2  2039  2eu4  2138  ralcomf  2658  gencbval  2812  unissb  3869  dfiin2g  3949  dftr5  4134  cotr  5051  cnvsym  5053  dffun2  5268  funcnveq  5321  fun11  5325