Theorem alcom 1489

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 1459	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-7 1459	. 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 1459

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1496  alrot4  1497  nfalt  1589  nfexd  1772  sbnf2  1997  sbcom2v  2001  sbalyz  2015  sbal1yz  2017  sbal2  2036  2eu4  2135  ralcomf  2655  gencbval  2808  unissb  3865  dfiin2g  3945  dftr5  4130  cotr  5047  cnvsym  5049  dffun2  5264  funcnveq  5317  fun11  5321