Theorem alcom 2162

Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2046 when it allows to avoid dependence on ax-11 2160. (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 209	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 206  ∀wal 1539

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 207

This theorem is referenced by:  alrot3  2163  excom  2165  sbal  2172  sbcom2  2176  nfa2  2179  aaan  2333  sb8v  2353  sb8f  2354  sbnf2  2358  sbal1  2528  sbal2  2529  2mo2  2642  ralcom4  3258  ralcom  3260  ralcomf  3270  sbccomlem  3815  dfiin2g  4976  fun11  6550  aceq1  10003  isch2  31195  dfon2lem8  35824  bj-hbaeb  36853  wl-sb9v  37583  wl-sbcom2d  37595  wl-sbalnae  37596  wl-2spsbbi  37599  cocossss  38473  cossssid3  38506  trcoss2  38521  dford4  43062  unielss  43251  elmapintrab  43609  undmrnresiss  43637  cnvssco  43639  elintima  43686  relexp0eq  43734  dfhe3  43808  dffrege115  44011  hbexg  44589  hbexgVD  44938  dfich2  47489  ichcom  47490