Theorem alcom 1526

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

Syntax hints:   ↔ wb 105  ∀wal 1395

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1533  alrot4  1534  nfalt  1626  nfexd  1809  sbnf2  2034  sbcom2v  2038  sbalyz  2052  sbal1yz  2054  sbal2  2073  2eu4  2173  ralcomf  2694  gencbval  2852  unissb  3923  dfiin2g  4003  dftr5  4190  cotr  5118  cnvsym  5120  dffun2  5336  funcnveq  5393  fun11  5397