Theorem bj-mp2c 32531

Description: A double modus ponens inference. Inference associated with mpd 15. (Contributed by BJ, 24-Sep-2019.)

Hypotheses

Ref	Expression
bj-mp2c.1	|- ph
bj-mp2c.2	|- ( ph -> ps )
bj-mp2c.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
bj-mp2c	|- ch

Proof of Theorem bj-mp2c

Step	Hyp	Ref	Expression
1		bj-mp2c.1	. 2 |- ph
2		bj-mp2c.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4		bj-mp2c.3	. 2 |- ( ph -> ( ps -> ch ) )
5	1, 3, 4	mp2 9	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by: (None)