Metamath Proof Explorer


Theorem wl-luk-imtrid

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

Ref Expression
Hypotheses wl-luk-imtrid.1 φ ψ
wl-luk-imtrid.2 χ ψ θ
Assertion wl-luk-imtrid χ φ θ

Proof

Step Hyp Ref Expression
1 wl-luk-imtrid.1 φ ψ
2 wl-luk-imtrid.2 χ ψ θ
3 1 wl-luk-imim1i ψ θ φ θ
4 2 3 wl-luk-syl χ φ θ