Theorem inegd 1417

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

Hypothesis

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

Assertion

Ref	Expression
inegd	|- ( ph -> -. ps )

Proof of Theorem inegd

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   F. wfal 1403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404

This theorem is referenced by:  genpdisj  7854  cauappcvgprlemdisj  7982  caucvgprlemdisj  8005  caucvgprprlemdisj  8033  suplocexprlemdisj  8051  suplocexprlemub  8054  suplocsrlem  8139  resqrexlemgt0  11730  resqrexlemoverl  11731  leabs  11784  climge0  12035  isprm5lem  12863  ennnfonelemex  13249  dedekindeu  15614  dedekindicclemicc  15623  usgr1vr  16369  pw1nct  16903