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  7742  cauappcvgprlemdisj  7870  caucvgprlemdisj  7893  caucvgprprlemdisj  7921  suplocexprlemdisj  7939  suplocexprlemub  7942  suplocsrlem  8027  resqrexlemgt0  11580  resqrexlemoverl  11581  leabs  11634  climge0  11885  isprm5lem  12712  ennnfonelemex  13034  dedekindeu  15346  dedekindicclemicc  15355  usgr1vr  16098  pw1nct  16604