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  2362  sb8v  2382  sb8f  2383  sbnf2  2387  sbal1  2557  sbal2  2558  2mo2  2672  ralcom4  3288  ralcom  3290  ralcomf  3300  sbccomlem  3817  dfiin2g  4989  fun11  6607  aceq1  10120  isch2  31704  dfon2lem8  36367  bj-hbaeb  37562  bj-axseprep  37819  wl-sb9v  38312  wl-sbcom2d  38324  wl-sbalnae  38325  wl-2spsbbi  38328  cocossss  39274  cossssid3  39307  trcoss2  39322  dford4  43870  unielss  44059  elmapintrab  44416  undmrnresiss  44444  cnvssco  44446  elintima  44493  relexp0eq  44541  dfhe3  44615  dffrege115  44818  hbexg  45379  hbexgVD  45728  dfich2  48358  ichcom  48359