ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  alcom GIF version

Theorem alcom 1383
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alcom (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)

Proof of Theorem alcom
StepHypRef Expression
1 ax-7 1353 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-7 1353 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 121 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 102  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105  ax-7 1353
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  alrot3  1390  alrot4  1391  nfalt  1486  nfexd  1660  sbnf2  1873  sbcom2v  1877  sbalyz  1891  sbal1yz  1893  sbal2  1914  2eu4  2009  ralcomf  2488  gencbval  2619  unissb  3638  dfiin2g  3718  dftr5  3885  cotr  4734  cnvsym  4736  dffun2  4940  funcnveq  4990  fun11  4994
  Copyright terms: Public domain W3C validator