Metamath Proof Explorer


Theorem bj-peircei

Description: Inference associated with peirce . (Contributed by BJ, 30-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 bj-peircei.1
 |-  ( ( ph -> ps ) -> ph )
2 peirce
 |-  ( ( ( ph -> ps ) -> ph ) -> ph )
3 1 2 ax-mp
 |-  ph