Metamath Proof Explorer


Theorem bj-nnclavci

Description: Inference associated with bj-nnclavc . Its associated inference is an instance of syl . Notice the non-intuitionistic proof from peirce and syl . (Contributed by BJ, 30-Jul-2024)

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

Proof

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