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  7840  cauappcvgprlemdisj  7968  caucvgprlemdisj  7991  caucvgprprlemdisj  8019  suplocexprlemdisj  8037  suplocexprlemub  8040  suplocsrlem  8125  resqrexlemgt0  11709  resqrexlemoverl  11710  leabs  11763  climge0  12014  isprm5lem  12842  ennnfonelemex  13182  dedekindeu  15505  dedekindicclemicc  15514  usgr1vr  16260  pw1nct  16794