jath

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

		Ref	Expression
	Assertion	jath	$⊢ (\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))$

Proof

Step	Hyp	Ref	Expression
1		jcn	$⊢ \neg φ \to (\neg χ \to \neg (\neg φ \to χ))$
2		pm2.21	$⊢ \neg (\neg φ \to χ) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
3		imim2	$⊢ (\neg (\neg φ \to χ) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg χ \to \neg (\neg φ \to χ)) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
4	2 3	ax-mp	$⊢ (\neg χ \to \neg (\neg φ \to χ)) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
5		imim2	$⊢ ((\neg χ \to \neg (\neg φ \to χ)) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to ((\neg φ \to (\neg χ \to \neg (\neg φ \to χ))) \to (\neg φ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))))$
6	4 5	ax-mp	$⊢ (\neg φ \to (\neg χ \to \neg (\neg φ \to χ))) \to (\neg φ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
7	1 6	ax-mp	$⊢ \neg φ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
8		ax-1	$⊢ χ \to ((φ \to ψ) \to χ)$
9		ax-1	$⊢ ((φ \to ψ) \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))$
10		imim2	$⊢ (((φ \to ψ) \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to ((χ \to ((φ \to ψ) \to χ)) \to (χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
11	9 10	ax-mp	$⊢ (χ \to ((φ \to ψ) \to χ)) \to (χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
12	8 11	ax-mp	$⊢ χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))$
13		ax-1	$⊢ ((ψ \to χ) \to ((φ \to ψ) \to χ)) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
14		imim2	$⊢ (((ψ \to χ) \to ((φ \to ψ) \to χ)) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
15	13 14	ax-mp	$⊢ (χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
16	12 15	ax-mp	$⊢ χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
17		pm2.61	$⊢ (χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
18	16 17	ax-mp	$⊢ (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
19		imim2	$⊢ ((\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (\neg φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
20	18 19	ax-mp	$⊢ (\neg φ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (\neg φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
21	7 20	ax-mp	$⊢ \neg φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
22		jcn	$⊢ φ \to (\neg ψ \to \neg (φ \to ψ))$
23		pm2.21	$⊢ \neg (φ \to ψ) \to ((φ \to ψ) \to χ)$
24		imim2	$⊢ (\neg (φ \to ψ) \to ((φ \to ψ) \to χ)) \to ((\neg ψ \to \neg (φ \to ψ)) \to (\neg ψ \to ((φ \to ψ) \to χ)))$
25	23 24	ax-mp	$⊢ (\neg ψ \to \neg (φ \to ψ)) \to (\neg ψ \to ((φ \to ψ) \to χ))$
26		imim2	$⊢ ((\neg ψ \to \neg (φ \to ψ)) \to (\neg ψ \to ((φ \to ψ) \to χ))) \to ((φ \to (\neg ψ \to \neg (φ \to ψ))) \to (φ \to (\neg ψ \to ((φ \to ψ) \to χ))))$
27	25 26	ax-mp	$⊢ (φ \to (\neg ψ \to \neg (φ \to ψ))) \to (φ \to (\neg ψ \to ((φ \to ψ) \to χ)))$
28	22 27	ax-mp	$⊢ φ \to (\neg ψ \to ((φ \to ψ) \to χ))$
29		imim2	$⊢ (((φ \to ψ) \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to ((\neg ψ \to ((φ \to ψ) \to χ)) \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
30	9 29	ax-mp	$⊢ (\neg ψ \to ((φ \to ψ) \to χ)) \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
31		imim2	$⊢ ((\neg ψ \to ((φ \to ψ) \to χ)) \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((φ \to (\neg ψ \to ((φ \to ψ) \to χ))) \to (φ \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
32	30 31	ax-mp	$⊢ (φ \to (\neg ψ \to ((φ \to ψ) \to χ))) \to (φ \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
33	28 32	ax-mp	$⊢ φ \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
34		imim2	$⊢ (((ψ \to χ) \to ((φ \to ψ) \to χ)) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
35	13 34	ax-mp	$⊢ (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
36		imim2	$⊢ ((\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to ((φ \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to (φ \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))))$
37	35 36	ax-mp	$⊢ (φ \to (\neg ψ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to (φ \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
38	33 37	ax-mp	$⊢ φ \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
39		jcn	$⊢ ψ \to (\neg χ \to \neg (ψ \to χ))$
40		pm2.21	$⊢ \neg (ψ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))$
41		imim2	$⊢ (\neg (ψ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to ((\neg χ \to \neg (ψ \to χ)) \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
42	40 41	ax-mp	$⊢ (\neg χ \to \neg (ψ \to χ)) \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
43		imim2	$⊢ ((\neg χ \to \neg (ψ \to χ)) \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((ψ \to (\neg χ \to \neg (ψ \to χ))) \to (ψ \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
44	42 43	ax-mp	$⊢ (ψ \to (\neg χ \to \neg (ψ \to χ))) \to (ψ \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
45	39 44	ax-mp	$⊢ ψ \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
46		imim2	$⊢ (((ψ \to χ) \to ((φ \to ψ) \to χ)) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
47	13 46	ax-mp	$⊢ (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
48		imim2	$⊢ ((\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ))) \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to ((ψ \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to (ψ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))))$
49	47 48	ax-mp	$⊢ (ψ \to (\neg χ \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to (ψ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
50	45 49	ax-mp	$⊢ ψ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
51		imim2	$⊢ ((\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((ψ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
52	18 51	ax-mp	$⊢ (ψ \to (\neg χ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
53	50 52	ax-mp	$⊢ ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
54		pm2.61	$⊢ (ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
55	53 54	ax-mp	$⊢ (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
56		imim2	$⊢ ((\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((φ \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))))$
57	55 56	ax-mp	$⊢ (φ \to (\neg ψ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))) \to (φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
58	38 57	ax-mp	$⊢ φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
59		pm2.61	$⊢ (φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))))$
60	58 59	ax-mp	$⊢ (\neg φ \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))) \to ((\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ)))$
61	21 60	ax-mp	$⊢ (\neg φ \to χ) \to ((ψ \to χ) \to ((φ \to ψ) \to χ))$

Metamath Proof Explorer

Theorem jath

Proof