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 ( ( ¬ 𝜑 → 𝜒 ) → ( ( 𝜓 → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜒 ) ) )

Proof

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