Theorem alcom 2156

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 2154	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-11 2154	. 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 2154

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  alrot3  2157  sbal  2159  sbcom2  2161  excom  2162  nfa2  2170  aaan  2328  sb8v  2350  sb8f  2351  sbnf2  2356  sbal1  2533  sbal2  2534  2mo2  2649  nfra2w  3153  nfra2wOLD  3154  ralcom4  3163  ralcom4OLD  3164  ralcom  3165  ralcomf  3282  moelOLD  3358  unissb  4875  dfiin2g  4964  dftr5  5196  cotrg  6018  cnvsym  6021  dffun2OLD  6446  fun11  6510  aceq1  9871  isch2  29582  dfon2lem8  33763  bj-hbaeb  34999  wl-sbcom2d  35713  wl-sbalnae  35714  wl-2spsbbi  35717  cocossss  36556  cossssid3  36584  trcoss2  36599  dford4  40848  elmapintrab  41154  undmrnresiss  41182  cnvssco  41184  elintima  41231  relexp0eq  41279  dfhe3  41353  dffrege115  41556  hbexg  42146  hbexgVD  42496  dfich2  44877  ichcom  44878