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  2849  unissb  3917  dfiin2g  3997  dftr5  4184  cotr  5109  cnvsym  5111  dffun2  5327  funcnveq  5383  fun11  5387