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  2770  unissb  3922  dfiin2g  4001  eqpw1  4163  pw111  4171  insklem  4305  ssfin  4471  ssopr  4847  cotr  5027  cnvsym  5028  fun11  5160  dff13  5472