Theorem inegd 1421

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   F. wfal 1407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-tru 1405  df-fal 1408

This theorem is used by:  genpdisj  7896  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  suplocexprlemdisj  8093  suplocexprlemub  8096  suplocsrlem  8181  resqrexlemgt0  11807  resqrexlemoverl  11808  leabs  11861  climge0  12115  isprm5lem  12944  ennnfonelemex  13362  dedekindeu  15866  dedekindicclemicc  15875  usgr1vr  16711  pw1nct  17255