Theorem wl-luk-ja

Description: Inference joining the antecedents of two premises. Copy of ja with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	wl-luk-ja.1	|- ( -. ph -> ch )
	wl-luk-ja.2	|- ( ps -> ch )
Assertion	wl-luk-ja	|- ( ( ph -> ps ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		wl-luk-ja.1	|- ( -. ph -> ch )
2		wl-luk-ja.2	|- ( ps -> ch )
3	1	wl-luk-con1i	|- ( -. ch -> ph )
4	2	wl-luk-imim2i	|- ( ( ph -> ps ) -> ( ph -> ch ) )
5	3 4	wl-luk-imtrid	|- ( ( ph -> ps ) -> ( -. ch -> ch ) )
6	5	wl-luk-pm2.18d	|- ( ( ph -> ps ) -> ch )