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 φ ψ χ θ ψ χ φ θ