Theorem alcom 1524

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

Syntax hints:   ↔ wb 105  ∀wal 1393

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1531  alrot4  1532  nfalt  1624  nfexd  1807  sbnf2  2032  sbcom2v  2036  sbalyz  2050  sbal1yz  2052  sbal2  2071  2eu4  2171  ralcomf  2692  gencbval  2850  unissb  3921  dfiin2g  4001  dftr5  4188  cotr  5116  cnvsym  5118  dffun2  5334  funcnveq  5390  fun11  5394