Theorem inegd 1416

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 1415	. 2 |- ( -. ps <-> ( ps -> F. ) )
4	2, 3	sylibr 134	1 |- ( ph -> -. ps )

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

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 1400  df-fal 1403

This theorem is referenced by:  genpdisj  7743  cauappcvgprlemdisj  7871  caucvgprlemdisj  7894  caucvgprprlemdisj  7922  suplocexprlemdisj  7940  suplocexprlemub  7943  suplocsrlem  8028  resqrexlemgt0  11598  resqrexlemoverl  11599  leabs  11652  climge0  11903  isprm5lem  12731  ennnfonelemex  13053  dedekindeu  15366  dedekindicclemicc  15375  usgr1vr  16118  pw1nct  16655