merlem13 - Metamath Proof Explorer

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

Theorem merlem13 1579

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

**Assertion**
Ref	Expression
merlem13

**Proof of Theorem merlem13**
Step	Hyp	Ref	Expression
1		merlem12 1578	. . . . 5
2		merlem12 1578	. . . . . . . 8
3		merlem5 1571	. . . . . . . 8
4	2, 3	ax-mp 5	. . . . . . 7
5		merlem6 1572	. . . . . . 7
6	4, 5	ax-mp 5	. . . . . 6
7		meredith 1566	. . . . . 6
8	6, 7	ax-mp 5	. . . . 5
9	1, 8	ax-mp 5	. . . 4
10		merlem6 1572	. . . 4
11	9, 10	ax-mp 5	. . 3
12		merlem11 1577	. . 3
13	11, 12	ax-mp 5	. 2
14		meredith 1566	. 2
15	13, 14	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: luk-1 1580

W3C validator