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	. 2 ⊢ ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
2		imim1 83	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))
3	1, 2	syl9r 78	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:  bj-nnfim1  36745  bj-nnfim2  36746