Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem merlem13 657

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 656	. . . . 5
2		merlem12 656	. . . . . . . 8
3		merlem5 649	. . . . . . . 8
4	2, 3	ax-mp 6	. . . . . . 7
5		merlem6 650	. . . . . . 7
6	4, 5	ax-mp 6	. . . . . 6
7		meredith 644	. . . . . 6
8	6, 7	ax-mp 6	. . . . 5
9	1, 8	ax-mp 6	. . . 4
10		merlem6 650	. . . 4
11	9, 10	ax-mp 6	. . 3
12		merlem11 655	. . 3
13	11, 12	ax-mp 6	. 2
14		meredith 644	. 2
15	13, 14	ax-mp 6	1

Colors of variables: wff set class

Syntax hints:

wn 1

wi 2

This theorem is referenced by: luk-1 658

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