Theorem alcom 2158

Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 30-Jun-1993.)

Assertion

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

Proof of Theorem alcom

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

Syntax hints:   ↔ wb 205  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  alrot3  2159  sbal  2161  sbcom2  2163  excom  2164  nfa2  2172  sbnf2  2356  sbal1  2533  sbal2  2534  2mo2  2649  nfra2w  3151  nfra2wOLD  3152  ralcom4  3161  ralcom4OLD  3162  ralcom  3280  ralcomf  3282  moel  3349  unissb  4870  dfiin2g  4958  dftr5  5190  cotrg  6005  cnvsym  6008  dffun2  6428  fun11  6492  aceq1  9804  isch2  29486  dfon2lem8  33672  bj-hbaeb  34929  wl-sbcom2d  35643  wl-sbalnae  35644  wl-2spsbbi  35647  cocossss  36486  cossssid3  36514  trcoss2  36529  dford4  40767  elmapintrab  41073  undmrnresiss  41101  cnvssco  41103  elintima  41150  relexp0eq  41198  dfhe3  41272  dffrege115  41475  hbexg  42065  hbexgVD  42415  dfich2  44798  ichcom  44799