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

Theorem alcom 1408
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 1378 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1378 . 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 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106  ax-7 1378
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  alrot3  1415  alrot4  1416  nfalt  1511  nfexd  1685  sbnf2  1899  sbcom2v  1903  sbalyz  1917  sbal1yz  1919  sbal2  1940  2eu4  2035  ralcomf  2516  gencbval  2648  unissb  3639  dfiin2g  3719  dftr5  3886  cotr  4736  cnvsym  4738  dffun2  4942  funcnveq  4993  fun11  4997
  Copyright terms: Public domain W3C validator