Theorem inegd 1421

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

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

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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408

This theorem is referenced by:  genpdisj  7880  cauappcvgprlemdisj  8008  caucvgprlemdisj  8031  caucvgprprlemdisj  8059  suplocexprlemdisj  8077  suplocexprlemub  8080  suplocsrlem  8165  resqrexlemgt0  11764  resqrexlemoverl  11765  leabs  11818  climge0  12069  isprm5lem  12897  ennnfonelemex  13283  dedekindeu  15647  dedekindicclemicc  15656  usgr1vr  16403  pw1nct  16947