merlem7 - Metamath Proof Explorer

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

Theorem merlem7 1573

Description: Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
merlem7

**Proof of Theorem merlem7**
Step	Hyp	Ref	Expression
1		merlem4 1570	. 2
2		merlem6 1572	. . . 4
3		meredith 1566	. . . 4
4	2, 3	ax-mp 5	. . 3
5		meredith 1566	. . 3
6	4, 5	ax-mp 5	. 2
7	1, 6	ax-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-1 6 ax-2 7 ax-3 8

This theorem is referenced by: merlem8 1574

W3C validator