Theorem alcom 1471

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

Syntax hints:   ↔ wb 104  ∀wal 1346

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1478  alrot4  1479  nfalt  1571  nfexd  1754  sbnf2  1974  sbcom2v  1978  sbalyz  1992  sbal1yz  1994  sbal2  2013  2eu4  2112  ralcomf  2631  gencbval  2778  unissb  3826  dfiin2g  3906  dftr5  4090  cotr  4992  cnvsym  4994  dffun2  5208  funcnveq  5261  fun11  5265