Theorem wl-ja 33261

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

Hypotheses

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

Assertion

Ref	Expression
wl-ja	|- ( ( ph -> ps ) -> ch )

Proof of Theorem wl-ja

Step	Hyp	Ref	Expression
1		wl-ja.1	. . . 4 |- ( -. ph -> ch )
2	1	wl-con1i 33260	. . 3 |- ( -. ch -> ph )
3		wl-ja.2	. . . 4 |- ( ps -> ch )
4	3	wl-imim2i 33253	. . 3 |- ( ( ph -> ps ) -> ( ph -> ch ) )
5	2, 4	wl-syl5 33247	. 2 |- ( ( ph -> ps ) -> ( -. ch -> ch ) )
6	5	wl-pm2.18d 33248	1 |- ( ( ph -> ps ) -> ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-luk1 33241  ax-luk2 33242  ax-luk3 33243

This theorem is referenced by:  wl-ax2  33264