Theorem inegd 1367

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

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

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 609  ax-in2 610

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354

This theorem is referenced by:  genpdisj  7474  cauappcvgprlemdisj  7602  caucvgprlemdisj  7625  caucvgprprlemdisj  7653  suplocexprlemdisj  7671  suplocexprlemub  7674  suplocsrlem  7759  resqrexlemgt0  10973  resqrexlemoverl  10974  leabs  11027  climge0  11277  isprm5lem  12084  ennnfonelemex  12358  dedekindeu  13356  dedekindicclemicc  13365  pw1nct  13998