Metamath Proof Explorer


Theorem imim12

Description: Closed form of imim12i and of 3syl . (Contributed by BJ, 16-Jul-2019)

Ref Expression
Assertion imim12 ( ( 𝜑𝜓 ) → ( ( 𝜒𝜃 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜃 ) ) ) )

Proof

Step Hyp Ref Expression
1 imim2 ( ( 𝜒𝜃 ) → ( ( 𝜓𝜒 ) → ( 𝜓𝜃 ) ) )
2 imim1 ( ( 𝜑𝜓 ) → ( ( 𝜓𝜃 ) → ( 𝜑𝜃 ) ) )
3 1 2 syl9r ( ( 𝜑𝜓 ) → ( ( 𝜒𝜃 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜃 ) ) ) )