Metamath Proof Explorer

Theorem axin1

Description: 'Not' introduction (intuitionistic logic axiom ax-in1). (Contributed by Jim Kingdon, 21-May-2018) (New usage is discouraged.)

Ref Expression
Assertion axin1 
|- ( ( ph -> -. ph ) -> -. ph )

Proof

Step Hyp Ref Expression
1 pm2.01 
 |-  ( ( ph -> -. ph ) -> -. ph )