Theorem alcom 2196

Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2078 when it allows to avoid dependence on ax-11 2194. (Contributed by NM, 30-Jun-1993.)

Assertion

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

Proof of Theorem alcom

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2194

This proof depends on definitions:  df-bi 210

This theorem is used by:  alrot3  2197  excom  2199  sbal  2206  sbcom2  2209  nfa2  2210  aaan  2363  sb8v  2383  sb8f  2384  sbnf2  2388  sbal1  2558  sbal2  2559  2mo2  2673  ralcom4  3289  ralcom  3291  ralcomf  3301  sbccomlem  3817  dfiin2g  4989  fun11  6612  aceq1  10189  isch2  31818  dfon2lem8  36532  bj-hbaeb  37711  bj-axseprep  37970  wl-sb9v  38461  wl-sbcom2d  38473  wl-sbalnae  38474  wl-2spsbbi  38477  cocossss  39438  cossssid3  39471  trcoss2  39486  dford4  44015  unielss  44204  elmapintrab  44561  undmrnresiss  44589  cnvssco  44591  elintima  44638  relexp0eq  44686  dfhe3  44760  dffrege115  44963  hbexg  45524  hbexgVD  45873  dfich2  48509  ichcom  48510