Theorem alcom 2194

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 209  ∀wal 1568

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  alrot3  2195  excom  2197  sbal  2204  sbcom2  2207  nfa2  2210  aaan  2365  sb8v  2385  sb8f  2386  sbnf2  2390  sbal1  2560  sbal2  2561  2mo2  2675  ralcom4  3291  ralcom  3293  ralcomf  3303  sbccomlem  3823  dfiin2g  4996  fun11  6612  aceq1  10102  isch2  31556  dfon2lem8  36261  bj-hbaeb  37435  bj-axseprep  37692  wl-sb9v  38185  wl-sbcom2d  38197  wl-sbalnae  38198  wl-2spsbbi  38201  cocossss  39156  cossssid3  39189  trcoss2  39204  dford4  43739  unielss  43928  elmapintrab  44285  undmrnresiss  44313  cnvssco  44315  elintima  44362  relexp0eq  44410  dfhe3  44484  dffrege115  44687  hbexg  45248  hbexgVD  45597  dfich2  48190  ichcom  48191