jath - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > jath		Structured version Visualization version Unicode version

Theorem jath 31609

Description: Closed form of ja 173. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)

**Assertion**
Ref	Expression
jath

**Proof of Theorem jath**
Step	Hyp	Ref	Expression
1		mth8 158	. . . 4
2		pm2.21 120	. . . . . 6
3		imim2 58	. . . . . 6
4	2, 3	ax-mp 5	. . . . 5
5		imim2 58	. . . . 5
6	4, 5	ax-mp 5	. . . 4
7	1, 6	ax-mp 5	. . 3
8		ax-1 6	. . . . . . 7
9		ax-1 6	. . . . . . . 8
10		imim2 58	. . . . . . . 8
11	9, 10	ax-mp 5	. . . . . . 7
12	8, 11	ax-mp 5	. . . . . 6
13		ax-1 6	. . . . . . 7
14		imim2 58	. . . . . . 7
15	13, 14	ax-mp 5	. . . . . 6
16	12, 15	ax-mp 5	. . . . 5
17		pm2.61 183	. . . . 5
18	16, 17	ax-mp 5	. . . 4
19		imim2 58	. . . 4
20	18, 19	ax-mp 5	. . 3
21	7, 20	ax-mp 5	. 2
22		mth8 158	. . . . . . 7
23		pm2.21 120	. . . . . . . . 9
24		imim2 58	. . . . . . . . 9
25	23, 24	ax-mp 5	. . . . . . . 8
26		imim2 58	. . . . . . . 8
27	25, 26	ax-mp 5	. . . . . . 7
28	22, 27	ax-mp 5	. . . . . 6
29		imim2 58	. . . . . . . 8
30	9, 29	ax-mp 5	. . . . . . 7
31		imim2 58	. . . . . . 7
32	30, 31	ax-mp 5	. . . . . 6
33	28, 32	ax-mp 5	. . . . 5
34		imim2 58	. . . . . . 7
35	13, 34	ax-mp 5	. . . . . 6
36		imim2 58	. . . . . 6
37	35, 36	ax-mp 5	. . . . 5
38	33, 37	ax-mp 5	. . . 4
39		mth8 158	. . . . . . . . 9
40		pm2.21 120	. . . . . . . . . . 11
41		imim2 58	. . . . . . . . . . 11
42	40, 41	ax-mp 5	. . . . . . . . . 10
43		imim2 58	. . . . . . . . . 10
44	42, 43	ax-mp 5	. . . . . . . . 9
45	39, 44	ax-mp 5	. . . . . . . 8
46		imim2 58	. . . . . . . . . 10
47	13, 46	ax-mp 5	. . . . . . . . 9
48		imim2 58	. . . . . . . . 9
49	47, 48	ax-mp 5	. . . . . . . 8
50	45, 49	ax-mp 5	. . . . . . 7
51		imim2 58	. . . . . . . 8
52	18, 51	ax-mp 5	. . . . . . 7
53	50, 52	ax-mp 5	. . . . . 6
54		pm2.61 183	. . . . . 6
55	53, 54	ax-mp 5	. . . . 5
56		imim2 58	. . . . 5
57	55, 56	ax-mp 5	. . . 4
58	38, 57	ax-mp 5	. . 3
59		pm2.61 183	. . 3
60	58, 59	ax-mp 5	. 2
61	21, 60	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: (None)

W3C validator