Theorem alcom 2162

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

Syntax hints:   ↔ wb 209  ∀wal 1541

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  alrot3  2163  sbal  2165  sbcom2  2167  excom  2168  nfa2  2176  sbnf2  2358  sbal1  2532  sbal2  2533  2mo2  2648  nfra2w  3139  ralcom4  3147  ralcom  3257  ralcomf  3259  moel  3325  unissb  4839  dfiin2g  4927  dftr5  5149  cotrg  5956  cnvsym  5959  dffun2  6368  fun11  6432  aceq1  9696  isch2  29258  dfon2lem8  33436  bj-hbaeb  34688  wl-sbcom2d  35402  wl-sbalnae  35403  wl-2spsbbi  35406  cocossss  36245  cossssid3  36273  trcoss2  36288  dford4  40495  elmapintrab  40801  undmrnresiss  40829  cnvssco  40831  elintima  40879  relexp0eq  40927  dfhe3  41001  dffrege115  41204  hbexg  41790  hbexgVD  42140  dfich2  44526  ichcom  44527