Theorem alcom 2195

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

Assertion

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

Proof of Theorem alcom

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

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

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

This proof depends on definitions:  df-bi 210

This theorem is used by:  alrot3  2196  excom  2198  sbal  2205  sbcom2  2208  nfa2  2209  aaan  2362  sb8v  2382  sb8f  2383  sbnf2  2387  sbal1  2557  sbal2  2558  2mo2  2672  ralcom4  3288  ralcom  3290  ralcomf  3300  sbccomlem  3816  dfiin2g  4988  fun11  6615  aceq1  10200  isch2  31831  dfon2lem8  36645  bj-hbaeb  37824  bj-axseprep  38083  wl-sb9v  38575  wl-sbcom2d  38587  wl-sbalnae  38588  wl-2spsbbi  38591  cocossss  39552  cossssid3  39585  trcoss2  39600  dford4  44130  unielss  44314  elmapintrab  44671  undmrnresiss  44698  cnvssco  44700  elintima  44747  relexp0eq  44795  dfhe3  44869  dffrege115  45072  hbexg  45633  hbexgVD  45982  dfich2  48634  ichcom  48635