# 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
`|- ( ( -. ph -> ch ) -> ( ( ps -> ch ) -> ( ( ph -> ps ) -> ch ) ) )`

### Proof

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