Theorem alcom 1737

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

Assertion

Ref	Expression
alcom	⊢ (∀x∀yφ ↔ ∀y∀xφ)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 1734	. 2 ⊢ (∀x∀yφ → ∀y∀xφ)
2		ax-7 1734	. 2 ⊢ (∀y∀xφ → ∀x∀yφ)
3	1, 2	impbii 180	1 ⊢ (∀x∀yφ ↔ ∀y∀xφ)

Syntax hints:   ↔ wb 176  ∀wal 1540

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  alrot3  1738  excom  1741  sbcom  2089  sbnf2  2108  sbcom2  2114  sbal2  2134  2mo  2282  2eu4  2287  ralcomf  2769  unissb  3921  dfiin2g  4000  eqpw1  4162  pw111  4170  insklem  4304  ssfin  4470  ssopr  4846  cotr  5026  cnvsym  5027  fun11  5159  dff13  5471