Theorem alcom 1465

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

Syntax hints:   ↔ wb 104  ∀wal 1340

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1472  alrot4  1473  nfalt  1565  nfexd  1748  sbnf2  1968  sbcom2v  1972  sbalyz  1986  sbal1yz  1988  sbal2  2007  2eu4  2106  ralcomf  2625  gencbval  2769  unissb  3813  dfiin2g  3893  dftr5  4077  cotr  4979  cnvsym  4981  dffun2  5192  funcnveq  5245  fun11  5249