merlem13 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem merlem13 936

Description: Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.

**Assertion**
Ref	Expression
merlem13

**Proof of Theorem merlem13**
Step	Hyp	Ref	Expression
1		merlem12 935	. . . . 5
2		merlem12 935	. . . . . . . 8
3		merlem5 928	. . . . . . . 8
4	2, 3	ax-mp 7	. . . . . . 7
5		merlem6 929	. . . . . . 7
6	4, 5	ax-mp 7	. . . . . 6
7		meredith 923	. . . . . 6
8	6, 7	ax-mp 7	. . . . 5
9	1, 8	ax-mp 7	. . . 4
10		merlem6 929	. . . 4
11	9, 10	ax-mp 7	. . 3
12		merlem11 934	. . 3
13	11, 12	ax-mp 7	. 2
14		meredith 923	. 2
15	13, 14	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

This theorem is referenced by: luk-1 937

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7