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  7485  cauappcvgprlemdisj  7613  caucvgprlemdisj  7636  caucvgprprlemdisj  7664  suplocexprlemdisj  7682  suplocexprlemub  7685  suplocsrlem  7770  resqrexlemgt0  10984  resqrexlemoverl  10985  leabs  11038  climge0  11288  isprm5lem  12095  ennnfonelemex  12369  dedekindeu  13395  dedekindicclemicc  13404  pw1nct  14036