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  7803  cauappcvgprlemdisj  7931  caucvgprlemdisj  7954  caucvgprprlemdisj  7982  suplocexprlemdisj  8000  suplocexprlemub  8003  suplocsrlem  8088  resqrexlemgt0  11660  resqrexlemoverl  11661  leabs  11714  climge0  11965  isprm5lem  12793  ennnfonelemex  13115  dedekindeu  15434  dedekindicclemicc  15443  usgr1vr  16189  pw1nct  16725