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  3154  nfra2wOLD  3155  ralcom4  3164  ralcom4OLD  3165  ralcom  3166  ralcomf  3283  moelOLD  3359  unissb  4873  dfiin2g  4962  dftr5  5194  cotrg  6016  cnvsym  6019  dffun2OLD  6444  fun11  6508  aceq1  9873  isch2  29585  dfon2lem8  33766  bj-hbaeb  35002  wl-sbcom2d  35716  wl-sbalnae  35717  wl-2spsbbi  35720  cocossss  36559  cossssid3  36587  trcoss2  36602  dford4  40851  elmapintrab  41184  undmrnresiss  41212  cnvssco  41214  elintima  41261  relexp0eq  41309  dfhe3  41383  dffrege115  41586  hbexg  42176  hbexgVD  42526  dfich2  44910  ichcom  44911