Metamath Proof Explorer


Theorem adh-minimp-sylsimp

Description: Derivation of jarr (also called "syll-simp") from minimp and ax-mp . Polish prefix notation: CCCpqrCqr . (Contributed by BJ, 4-Apr-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minimp-sylsimp ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 adh-minimp-jarr-ax2c-lem3 ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) )
2 adh-minimp-jarr-imim1-ax2c-lem1 ( ( ( 𝜑𝜓 ) → ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) ) → ( ( ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜑𝜓 ) ) → ( ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) )
3 adh-minimp-jarr-lem2 ( ( ( ( 𝜑𝜓 ) → ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) ) → ( ( ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜑𝜓 ) ) → ( ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) ) → ( ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) )
4 2 3 ax-mp ( ( ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) → ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) ) ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) )
5 1 4 ax-mp ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) )
6 adh-minimp-jarr-imim1-ax2c-lem1 ( ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) → ( ( ( 𝜓 → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) → ( 𝜓𝜒 ) ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) ) ) )
7 adh-minimp-jarr-lem2 ( ( ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) ) → ( ( ( 𝜓 → ( ( 𝜑𝜓 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) → ( 𝜓𝜒 ) ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) ) ) ) → ( ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) ) ) )
8 6 7 ax-mp ( ( ( 𝜑𝜓 ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → 𝜒 ) ) → ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) ) )
9 5 8 ax-mp ( ( ( 𝜑𝜓 ) → 𝜒 ) → ( 𝜓𝜒 ) )