Theorem alcom 1454

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

Syntax hints:   ↔ wb 104  ∀wal 1329

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1461  alrot4  1462  nfalt  1557  nfexd  1734  sbnf2  1956  sbcom2v  1960  sbalyz  1974  sbal1yz  1976  sbal2  1997  2eu4  2092  ralcomf  2592  gencbval  2734  unissb  3766  dfiin2g  3846  dftr5  4029  cotr  4920  cnvsym  4922  dffun2  5133  funcnveq  5186  fun11  5190