Metamath Proof Explorer

Theorem bj-poni

Description: Inference associated with "pon", pm2.27 . Its associated inference is ax-mp . (Contributed by BJ, 30-Jul-2024)

Ref Expression
Hypothesis bj-poni.1 
|- ph
Assertion bj-poni 
|- ( ( ph -> ps ) -> ps )

Proof

Step Hyp Ref Expression
1 bj-poni.1 
 |-  ph
2 pm2.27 
 |-  ( ph -> ( ( ph -> ps ) -> ps ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ps ) -> ps )