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

Theorem alcom 1367
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 1337 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1337 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 117 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 98   A.wal 1241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101  ax-7 1337
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  alrot3  1374  alrot4  1375  nfalt  1470  nfexd  1644  sbnf2  1857  sbcom2v  1861  sbalyz  1875  sbal1yz  1877  sbal2  1898  2eu4  1993  ralcomf  2471  gencbval  2602  unissb  3610  dfiin2g  3690  dftr5  3857  cotr  4706  cnvsym  4708  dffun2  4912  funcnveq  4962  fun11  4966
  Copyright terms: Public domain W3C validator