Theorem imim12 106

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

Assertion

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

Proof of Theorem imim12

Step	Hyp	Ref	Expression
1		imim2 59	. 2 ⊢ ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
2		imim1 84	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))
3	1, 2	syl9r 79	1 ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜑 → 𝜃))))

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:  bj-nnfim1  37623  bj-nnfim2  37624