Metamath Proof Explorer

Theorem inegd

Description: Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017)

Ref Expression
Hypothesis inegd.1 
|- ( ( ph /\ ps ) -> F. )
Assertion inegd 
|- ( ph -> -. ps )

Proof

Step Hyp Ref Expression
1 inegd.1 
 |-  ( ( ph /\ ps ) -> F. )
2 1 ex 
 |-  ( ph -> ( ps -> F. ) )
3 dfnot 
 |-  ( -. ps <-> ( ps -> F. ) )
4 2 3 sylibr 
 |-  ( ph -> -. ps )