Metamath Proof Explorer


Theorem bj-peircei

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

Ref Expression
Hypothesis bj-peircei.1 ( ( 𝜑𝜓 ) → 𝜑 )
Assertion bj-peircei 𝜑

Proof

Step Hyp Ref Expression
1 bj-peircei.1 ( ( 𝜑𝜓 ) → 𝜑 )
2 peirce ( ( ( 𝜑𝜓 ) → 𝜑 ) → 𝜑 )
3 1 2 ax-mp 𝜑