Theorem alcom 2163

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

Syntax hints:   ↔ wb 208  ∀wal 1535

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  alrot3  2164  sbal  2166  sbcom2  2168  excom  2169  nfa2  2176  sbnf2  2377  sbal1  2572  sbal2  2573  sbal2OLD  2574  2mo2  2732  ralcom4  3235  ralcom  3354  ralcomf  3357  unissb  4870  dfiin2g  4957  dftr5  5175  cotrg  5971  cnvsym  5974  dffun2  6365  fun11  6428  aceq1  9543  isch2  29000  moel  30252  dfon2lem8  33035  bj-hbaeb  34142  wl-sbcom2d  34812  wl-sbalnae  34813  wl-2spsbbi  34816  wl-dfralflem  34853  cocossss  35696  cossssid3  35724  trcoss2  35739  dford4  39646  elmapintrab  39956  undmrnresiss  39984  cnvssco  39986  elintima  40018  relexp0eq  40066  dfhe3  40141  dffrege115  40344  hbexg  40910  hbexgVD  41260  dfich2  43633  dfich2ai  43634  ichcom  43637