Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  renicax Structured version   Unicode version

Theorem renicax 1574
 Description: A rederivation of nic-ax 1550 from lukshef-ax1 1571, proving that lukshef-ax1 1571 with nic-mp 1548 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
renicax

Proof of Theorem renicax
StepHypRef Expression
1 lukshefth1 1572 . . . 4
2 lukshefth2 1573 . . . 4
31, 2nic-mp 1548 . . 3
4 lukshefth2 1573 . . . 4
5 lukshef-ax1 1571 . . . 4
64, 5nic-mp 1548 . . 3
73, 6nic-mp 1548 . 2
8 lukshefth2 1573 . 2
97, 8nic-mp 1548 1
 Colors of variables: wff setvar class Syntax hints:   wnan 1379 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 188  df-an 372  df-nan 1380 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator