Metamath Proof Explorer

Theorem minimp-ax2c

Description: Derivation of a commuted form of ax-2 from ax-mp and minimp . (Contributed by BJ, 4-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion minimp-ax2c ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 minimp ⊢ ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) )
2 minimp ⊢ ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) )
3 1 2 ax-mp ⊢ ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
4 minimp ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) ) )
5 minimp ⊢ ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) ) )
6 minimp ⊢ ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) )
7 minimp ⊢ ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) ) ) )
8 minimp ⊢ ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) )
9 minimp ⊢ ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) )
10 7 8 9 mp2 ⊢ ( ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) )
11 minimp ⊢ ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → 𝜑 ) ) ) )
12 5 11 ax-mp ⊢ ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( ( 𝜑 → ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → 𝜑 ) ) )
13 6 10 12 mp2 ⊢ ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → 𝜑 )
14 minimp ⊢ ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → 𝜑 ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) ) )
15 5 13 14 mp2 ⊢ ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) )
16 minimp-syllsimp ⊢ ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) )
17 15 16 ax-mp ⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) )
18 minimp ⊢ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) ) ) ) → ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) )
19 4 17 18 mp2 ⊢ ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
20 minimp-syllsimp ⊢ ( ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) )
21 19 20 ax-mp ⊢ ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
22 minimp ⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) )
23 minimp ⊢ ( ( 𝜑 → 𝜓 ) → ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) ) )
24 minimp ⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) )
25 23 24 ax-mp ⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) )
26 minimp ⊢ ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) → ( ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) ) )
27 22 25 26 mp2 ⊢ ( ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) )
28 minimp-syllsimp ⊢ ( ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) )
29 minimp-syllsimp ⊢ ( ( ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) → ( ( ( ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) ) ) )
30 27 28 29 mp2 ⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜑 → 𝜑 ) → ( ( ( 𝜑 → 𝜑 ) → ( 𝜑 → 𝜑 ) ) → ( 𝜑 → 𝜑 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) )
31 3 21 30 mp2 ⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )