Theorem alcom 2037

Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 30-Jun-1993.)

Assertion

Ref	Expression
alcom	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-11 2034	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-11 2034	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 199	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 196  ∀wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2034

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  alrot3  2038  nfa2  2040  excom  2042  sbnf2  2439  sbcom2  2445  sbal1  2460  sbal2  2461  2mo2  2550  ralcomf  3096  unissb  4469  dfiin2g  4553  dftr5  4755  cotrg  5507  cnvsym  5510  dffun2  5898  fun11  5963  aceq1  8940  isch2  28080  moel  29323  dfon2lem8  31695  bj-ssb1  32633  bj-hbaeb  32806  bj-ralcom4  32868  wl-sbcom2d  33344  wl-sbalnae  33345  dford4  37596  elmapintrab  37882  undmrnresiss  37910  cnvssco  37912  elintima  37945  relexp0eq  37993  dfhe3  38069  dffrege115  38272  hbexg  38772  hbexgVD  39142