Theorem inegd 1362

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 114	. 2 |- ( ph -> ( ps -> F. ) )
3		dfnot 1361	. 2 |- ( -. ps <-> ( ps -> F. ) )
4	2, 3	sylibr 133	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   F. wfal 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-fal 1349

This theorem is referenced by:  genpdisj  7464  cauappcvgprlemdisj  7592  caucvgprlemdisj  7615  caucvgprprlemdisj  7643  suplocexprlemdisj  7661  suplocexprlemub  7664  suplocsrlem  7749  resqrexlemgt0  10962  resqrexlemoverl  10963  leabs  11016  climge0  11266  isprm5lem  12073  ennnfonelemex  12347  dedekindeu  13241  dedekindicclemicc  13250  pw1nct  13883