merlem13 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > merlem13		Unicode version

Theorem merlem13 1419

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 1418	. . . . 5
2		merlem12 1418	. . . . . . . 8
3		merlem5 1411	. . . . . . . 8
4	2, 3	ax-mp 5	. . . . . . 7
5		merlem6 1412	. . . . . . 7
6	4, 5	ax-mp 5	. . . . . 6
7		ax-meredith 1406	. . . . . 6
8	6, 7	ax-mp 5	. . . . 5
9	1, 8	ax-mp 5	. . . 4
10		merlem6 1412	. . . 4
11	9, 10	ax-mp 5	. . 3
12		merlem11 1417	. . 3
13	11, 12	ax-mp 5	. 2
14		ax-meredith 1406	. 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-meredith 1406

This theorem is referenced by: luk-1 1420

W3C validator