Metamath Proof Explorer


Theorem wl-luk-imtrdi

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. Copy of syl6 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses wl-luk-imtrdi.1 ( 𝜑 → ( 𝜓𝜒 ) )
wl-luk-imtrdi.2 ( 𝜒𝜃 )
Assertion wl-luk-imtrdi ( 𝜑 → ( 𝜓𝜃 ) )

Proof

Step Hyp Ref Expression
1 wl-luk-imtrdi.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 wl-luk-imtrdi.2 ( 𝜒𝜃 )
3 2 wl-luk-imim2i ( ( 𝜓𝜒 ) → ( 𝜓𝜃 ) )
4 1 3 wl-luk-syl ( 𝜑 → ( 𝜓𝜃 ) )