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

Theorem renicax 1471
 Description: A rederivation of nic-ax 1447 from lukshef-ax1 1468, proving that lukshef-ax1 1468 with nic-mp 1445 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 1469 . . . 4
2 lukshefth2 1470 . . . 4
31, 2nic-mp 1445 . . 3
4 lukshefth2 1470 . . . 4
5 lukshef-ax1 1468 . . . 4
64, 5nic-mp 1445 . . 3
73, 6nic-mp 1445 . 2
8 lukshefth2 1470 . 2
97, 8nic-mp 1445 1
 Colors of variables: wff set class Syntax hints:   wnan 1296 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361  df-nan 1297
 Copyright terms: Public domain W3C validator