Metamath Proof Explorer


Theorem imbitrid

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993)

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

Proof

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