Theorem alcom 1502

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

Syntax hints:   ↔ wb 105  ∀wal 1371

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1509  alrot4  1510  nfalt  1602  nfexd  1785  sbnf2  2010  sbcom2v  2014  sbalyz  2028  sbal1yz  2030  sbal2  2049  2eu4  2148  ralcomf  2668  gencbval  2823  unissb  3886  dfiin2g  3966  dftr5  4153  cotr  5073  cnvsym  5075  dffun2  5290  funcnveq  5346  fun11  5350