Theorem imim12 105

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

Assertion

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

Proof of Theorem imim12

Step	Hyp	Ref	Expression
1		imim2 58	. . . 4 ⊢ ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
2	1	com13 88	. . 3 ⊢ (𝜓 → ((𝜓 → 𝜒) → ((𝜒 → 𝜃) → 𝜃)))
3	2	imim2i 16	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → ((𝜓 → 𝜒) → ((𝜒 → 𝜃) → 𝜃))))
4	3	com24 95	1 ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜑 → 𝜃))))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by: (None)