Metamath Proof Explorer

Theorem bj-mp2d

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

Ref Expression
Hypotheses bj-mp2d.1 
|- ph
bj-mp2d.2 
|- ( ph -> ps )
bj-mp2d.3 
|- ( ps -> ( ph -> ch ) )
Assertion bj-mp2d 
|- ch

Proof

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