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

Theorem alcom 1412
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 1382 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1382 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 124 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106  ax-7 1382
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  alrot3  1419  alrot4  1420  nfalt  1515  nfexd  1691  sbnf2  1905  sbcom2v  1909  sbalyz  1923  sbal1yz  1925  sbal2  1946  2eu4  2041  ralcomf  2528  gencbval  2667  unissb  3683  dfiin2g  3763  dftr5  3939  cotr  4813  cnvsym  4815  dffun2  5025  funcnveq  5077  fun11  5081
  Copyright terms: Public domain W3C validator