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  2809  unissb  3866  dfiin2g  3946  dftr5  4131  cotr  5048  cnvsym  5050  dffun2  5265  funcnveq  5318  fun11  5322