Theorem alcom 1476

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

Syntax hints:   ↔ wb 105  ∀wal 1351

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1483  alrot4  1484  nfalt  1576  nfexd  1759  sbnf2  1979  sbcom2v  1983  sbalyz  1997  sbal1yz  1999  sbal2  2018  2eu4  2117  ralcomf  2636  gencbval  2783  unissb  3835  dfiin2g  3915  dftr5  4099  cotr  5002  cnvsym  5004  dffun2  5218  funcnveq  5271  fun11  5275