Theorem alcom 1527

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

Syntax hints:   ↔ wb 105  ∀wal 1396

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  alrot3  1534  alrot4  1535  nfalt  1627  nfexd  1810  sbnf2  2037  sbcom2v  2041  sbalyz  2055  sbal1yz  2057  sbal2  2076  2eu4  2176  ralcomf  2706  gencbval  2865  unissb  3949  dfiin2g  4029  dftr5  4216  cotr  5149  cnvsym  5151  dffun2  5367  funcnveq  5424  fun11  5428