Theorem alcom 2159

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

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  alrot3  2160  excom  2162  sbal  2169  sbcom2  2173  nfa2  2176  aaan  2332  sb8v  2354  sb8f  2355  sbnf2  2360  sbal1  2532  sbal2  2533  2mo2  2646  ralcom4  3268  ralcom  3270  ralcomf  3282  moelOLD  3384  sbccomlem  3844  unissbOLD  4916  dfiin2g  5008  dftr5OLD  5234  cotrgOLD  6097  cotrgOLDOLD  6098  cnvsymOLD  6102  cnvsymOLDOLD  6103  dffun2OLD  6542  dffun2OLDOLD  6543  fun11  6610  aceq1  10131  isch2  31204  dfon2lem8  35808  bj-hbaeb  36837  wl-sb9v  37567  wl-sbcom2d  37579  wl-sbalnae  37580  wl-2spsbbi  37583  cocossss  38454  cossssid3  38487  trcoss2  38502  dford4  43053  unielss  43242  elmapintrab  43600  undmrnresiss  43628  cnvssco  43630  elintima  43677  relexp0eq  43725  dfhe3  43799  dffrege115  44002  hbexg  44581  hbexgVD  44930  dfich2  47472  ichcom  47473