Theorem inegd 1382

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

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

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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-fal 1369

This theorem is referenced by:  genpdisj  7536  cauappcvgprlemdisj  7664  caucvgprlemdisj  7687  caucvgprprlemdisj  7715  suplocexprlemdisj  7733  suplocexprlemub  7736  suplocsrlem  7821  resqrexlemgt0  11043  resqrexlemoverl  11044  leabs  11097  climge0  11347  isprm5lem  12155  ennnfonelemex  12429  dedekindeu  14397  dedekindicclemicc  14406  pw1nct  15049