# Metamath Proof Explorer

## Theorem 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 ${⊢}\left(¬{\phi }\to {\chi }\right)\to \left(\left({\psi }\to {\chi }\right)\to \left(\left({\phi }\to {\psi }\right)\to {\chi }\right)\right)$

### Proof

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