Theorem alcom 1478

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 1448	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-7 1448	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 126	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 105  ∀wal 1351

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1485  alrot4  1486  nfalt  1578  nfexd  1761  sbnf2  1981  sbcom2v  1985  sbalyz  1999  sbal1yz  2001  sbal2  2020  2eu4  2119  ralcomf  2638  gencbval  2785  unissb  3838  dfiin2g  3918  dftr5  4102  cotr  5007  cnvsym  5009  dffun2  5223  funcnveq  5276  fun11  5280