Theorem jath 33672

Description: Closed form of ja 186. 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		jcn 162	. . . 4 ⊢ (¬ 𝜑 → (¬ 𝜒 → ¬ (¬ 𝜑 → 𝜒)))
2		pm2.21 123	. . . . . 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 191	. . . . 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		jcn 162	. . . . . . 7 ⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓)))
23		pm2.21 123	. . . . . . . . 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		jcn 162	. . . . . . . . 9 ⊢ (𝜓 → (¬ 𝜒 → ¬ (𝜓 → 𝜒)))
40		pm2.21 123	. . . . . . . . . . 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 191	. . . . . 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 191	. . 3 ⊢ ((𝜑 → ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))) → ((¬ 𝜑 → ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))) → ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))))
60	58, 59	ax-mp 5	. 2 ⊢ ((¬ 𝜑 → ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))) → ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒))))
61	21, 60	ax-mp 5	1 ⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))

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)