Theorem alcom 1500

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

Syntax hints:   ↔ wb 105  ∀wal 1370

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1507  alrot4  1508  nfalt  1600  nfexd  1783  sbnf2  2008  sbcom2v  2012  sbalyz  2026  sbal1yz  2028  sbal2  2047  2eu4  2146  ralcomf  2666  gencbval  2820  unissb  3879  dfiin2g  3959  dftr5  4144  cotr  5061  cnvsym  5063  dffun2  5278  funcnveq  5331  fun11  5335