Theorem alcom 1364

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 1334	. 2 ⊢ (∀x∀yφ → ∀y∀xφ)
2		ax-7 1334	. 2 ⊢ (∀y∀xφ → ∀x∀yφ)
3	1, 2	impbii 117	1 ⊢ (∀x∀yφ ↔ ∀y∀xφ)

Syntax hints:   ↔ wb 98  ∀wal 1240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101  ax-7 1334

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  alrot3  1371  alrot4  1372  nfalt  1467  nfexd  1641  sbnf2  1854  sbcom2v  1858  sbalyz  1872  sbal1yz  1874  sbal2  1895  2eu4  1990  ralcomf  2465  gencbval  2596  unissb  3601  dfiin2g  3681  dftr5  3848  cotr  4649  cnvsym  4651  dffun2  4855  funcnveq  4905  fun11  4909