Metamath Proof Explorer


Theorem syl5ib

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

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

Proof

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