Theorem alcom 1367

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

Assertion

Ref	Expression
alcom	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 1337	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
2		ax-7 1337	. 2 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
3	1, 2	impbii 117	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)

Syntax hints:   ↔ wb 98  ∀wal 1241

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  alrot3  1374  alrot4  1375  nfalt  1470  nfexd  1644  sbnf2  1857  sbcom2v  1861  sbalyz  1875  sbal1yz  1877  sbal2  1898  2eu4  1993  ralcomf  2471  gencbval  2602  unissb  3610  dfiin2g  3690  dftr5  3857  cotr  4706  cnvsym  4708  dffun2  4912  funcnveq  4962  fun11  4966