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

Theorem alcom 1455
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 1425 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-7 1425 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 125 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-7 1425
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  alrot3  1462  alrot4  1463  nfalt  1558  nfexd  1735  sbnf2  1957  sbcom2v  1961  sbalyz  1975  sbal1yz  1977  sbal2  1998  2eu4  2093  ralcomf  2595  gencbval  2737  unissb  3773  dfiin2g  3853  dftr5  4036  cotr  4927  cnvsym  4929  dffun2  5140  funcnveq  5193  fun11  5197
  Copyright terms: Public domain W3C validator