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

Theorem alcom 1478
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alcom  |-  ( A. x A. y ph  <->  A. y A. x ph )

Proof of Theorem alcom
StepHypRef Expression
1 ax-7 1448 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1448 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 126 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 105   A.wal 1351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-7 1448
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  alrot3  1485  alrot4  1486  nfalt  1578  nfexd  1761  sbnf2  1981  sbcom2v  1985  sbalyz  1999  sbal1yz  2001  sbal2  2020  2eu4  2119  ralcomf  2638  gencbval  2787  unissb  3841  dfiin2g  3921  dftr5  4106  cotr  5012  cnvsym  5014  dffun2  5228  funcnveq  5281  fun11  5285
  Copyright terms: Public domain W3C validator