Theorem alcom 2205

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 2202	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-11 2202	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 200	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 197  ∀wal 1635

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

This theorem depends on definitions:  df-bi 198

This theorem is referenced by:  alrot3  2206  nfa2  2208  excom  2210  sbnf2  2604  sbcom2  2608  sbal1  2623  sbal2  2624  nexmo  2640  2mo2  2725  ralcomf  3295  unissb  4674  dfiin2g  4756  dftr5  4960  cotrg  5731  cnvsym  5735  dffun2  6121  fun11  6184  aceq1  9233  isch2  28431  moel  29674  dfon2lem8  32037  bj-ssb1  32971  bj-hbaeb  33138  bj-ralcom4  33195  wl-sbcom2d  33677  wl-sbalnae  33678  cocossss  34523  cossssid3  34551  trcoss2  34566  dford4  38115  elmapintrab  38400  undmrnresiss  38428  cnvssco  38430  elintima  38463  relexp0eq  38511  dfhe3  38587  dffrege115  38790  hbexg  39288  hbexgVD  39654