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

Theorem alcom 1364
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 1334 . 2
2 ax-7 1334 . 2
31, 2impbii 117 1
Colors of variables: wff set class
Syntax hints:   wb 98  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101  ax-7 1334
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  alrot3  1371  alrot4  1372  nfalt  1467  nfexd  1641  sbnf2  1854  sbcom2v  1858  sbalyz  1872  sbal1yz  1874  sbal2  1895  2eu4  1990  ralcomf  2465  gencbval  2596  unissb  3601  dfiin2g  3681  dftr5  3848  cotr  4649  cnvsym  4651  dffun2  4855  funcnveq  4905  fun11  4909
  Copyright terms: Public domain W3C validator