Theorem alcom 1531

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

Syntax hints:   ↔ wb 105  ∀wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-7 1501

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1538  alrot4  1539  nfalt  1631  nfexd  1814  sbnf2  2041  sbcom2v  2045  sbalyz  2059  sbal1yz  2061  sbal2  2080  2eu4  2180  ralcomf  2712  gencbval  2871  unissb  3960  dfiin2g  4040  dftr5  4227  cotr  5164  cnvsym  5166  dffun2  5382  funcnveq  5439  fun11  5443