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

Theorem luklem1 1268
Description: Used to rederive standard propositional axioms from Lukasiewicz'.
Hypotheses
Ref Expression
luklem1.1
luklem1.2
Assertion
Ref Expression
luklem1

Proof of Theorem luklem1
StepHypRef Expression
1 luklem1.2 . 2
2 luklem1.1 . . 3
3 luk-1 1265 . . 3
42, 3ax-mp 8 . 2
51, 4ax-mp 8 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem is referenced by:  luklem2  1269  luklem3  1270  luklem4  1271  luklem5  1272  luklem6  1273  luklem7  1274  ax2  1277  ax3  1278
This theorem was proved from axioms:  ax-mp 8  ax-meredith 1251
  Copyright terms: Public domain W3C validator