Metamath Proof Explorer


Theorem syl5ibcom

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007)

Ref Expression
Hypotheses imbitrid.1 ( 𝜑𝜓 )
imbitrid.2 ( 𝜒 → ( 𝜓𝜃 ) )
Assertion syl5ibcom ( 𝜑 → ( 𝜒𝜃 ) )

Proof

Step Hyp Ref Expression
1 imbitrid.1 ( 𝜑𝜓 )
2 imbitrid.2 ( 𝜒 → ( 𝜓𝜃 ) )
3 1 2 imbitrid ( 𝜒 → ( 𝜑𝜃 ) )
4 3 com12 ( 𝜑 → ( 𝜒𝜃 ) )