New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  luk-2 GIF version

Theorem luk-2 1421
 Description: 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
luk-2 ((¬ φφ) → φ)

Proof of Theorem luk-2
StepHypRef Expression
1 merlem5 1411 . . . . 5 ((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ)))
2 merlem4 1410 . . . . 5 (((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ)))
31, 2ax-mp 5 . . . 4 ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ))
4 merlem11 1417 . . . 4 (((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ)) → ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ))
53, 4ax-mp 5 . . 3 ((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ)
6 ax-meredith 1406 . . 3 (((((φ → ¬ (¬ φφ)) → (¬ ¬ φ → ¬ (¬ φφ))) → ¬ φ) → ¬ φ) → ((¬ φφ) → ((¬ φφ) → φ)))
75, 6ax-mp 5 . 2 ((¬ φφ) → ((¬ φφ) → φ))
8 merlem11 1417 . 2 (((¬ φφ) → ((¬ φφ) → φ)) → ((¬ φφ) → φ))
97, 8ax-mp 5 1 ((¬ φφ) → φ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-meredith 1406 This theorem is referenced by:  luklem4  1426
 Copyright terms: Public domain W3C validator