Theorem inegd 1372

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

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

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

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359

This theorem is referenced by:  genpdisj  7524  cauappcvgprlemdisj  7652  caucvgprlemdisj  7675  caucvgprprlemdisj  7703  suplocexprlemdisj  7721  suplocexprlemub  7724  suplocsrlem  7809  resqrexlemgt0  11031  resqrexlemoverl  11032  leabs  11085  climge0  11335  isprm5lem  12143  ennnfonelemex  12417  dedekindeu  14186  dedekindicclemicc  14195  pw1nct  14837