Theorem alcom 1466

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

Syntax hints:   ↔ wb 104  ∀wal 1341

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1473  alrot4  1474  nfalt  1566  nfexd  1749  sbnf2  1969  sbcom2v  1973  sbalyz  1987  sbal1yz  1989  sbal2  2008  2eu4  2107  ralcomf  2627  gencbval  2774  unissb  3819  dfiin2g  3899  dftr5  4083  cotr  4985  cnvsym  4987  dffun2  5198  funcnveq  5251  fun11  5255