MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minimp-syllsimp Structured version   Visualization version   GIF version
Theorem minimp-syllsimp 1655
Description: Derivation of Syll-Simp (jarr 107) from ax-mp 5 and minimp 1654. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
minimp-syllsimp (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Proof of Theorem minimp-syllsimp
StepHypRef Expression
1 minimp 1654 . . 3 ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))
2 minimp 1654 . . . 4 ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))))))
3 minimp 1654 . . . 4 (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)))))
42, 3ax-mp 5 . . 3 (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))))
5 minimp 1654 . . . 4 (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))))))
6 minimp 1654 . . . 4 (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))
7 minimp 1654 . . . 4 ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)))))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → (((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))))
85, 6, 7mp2 9 . . 3 (((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))
91, 4, 8mp2b 10 . 2 (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))
10 minimp 1654 . . 3 ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))
11 minimp 1654 . . 3 (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))))
12 minimp 1654 . . . 4 ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → ((((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))))))
13 minimp 1654 . . . 4 ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))))
14 minimp 1654 . . . 4 (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → ((((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)))))) → (((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → ((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))) → ((((𝜑 → 𝜓) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))))))
1512, 13, 14mp2 9 . . 3 ((((𝜑 → 𝜓) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) → (((((𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))))
1610, 11, 15mp2b 10 . 2 ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))
17 minimp 1654 . . 3 (((𝜑 → 𝜓) → 𝜒) → ((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))))
18 minimp 1654 . . 3 ((((𝜑 → 𝜓) → 𝜒) → ((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) → (((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))))) → ((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((𝜓 → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (𝜓 → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)))))
19 minimp 1654 . . . 4 (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))))))
20 minimp 1654 . . . 4 (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜓 → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (𝜓 → 𝜒))))
21 minimp 1654 . . . 4 ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)))))) → ((((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → ((𝜓 → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (𝜓 → 𝜒)))) → (((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((𝜓 → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (𝜓 → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))))))
2219, 20, 21mp2 9 . . 3 (((((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒))) → (((𝜓 → ((𝜑 → 𝜓) → 𝜒)) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (𝜓 → 𝜒))) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)))) → (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))))
2317, 18, 22mp2b 10 . 2 (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → 𝜒) → 𝜒)) → (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)))
249, 16, 23mp2b 10 1 (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is used by:  minimp-ax1  1656  minimp-ax2c  1657  minimp-ax2  1658
  Copyright terms: Public domain W3C validator