Theorem alcom 1422

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

Syntax hints:   ↔ wb 104  ∀wal 1297

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  alrot3  1429  alrot4  1430  nfalt  1525  nfexd  1702  sbnf2  1917  sbcom2v  1921  sbalyz  1935  sbal1yz  1937  sbal2  1958  2eu4  2053  ralcomf  2550  gencbval  2689  unissb  3713  dfiin2g  3793  dftr5  3969  cotr  4856  cnvsym  4858  dffun2  5069  funcnveq  5122  fun11  5126