Theorem dfnot 1332

Description: Given falsum, we can define the negation of a wff ph as the statement that a contradiction follows from assuming ph. (Contributed by Mario Carneiro, 9-Feb-2017.)

Assertion

Ref	Expression
dfnot	|- (-. ph <-> (ph -> F. ))

Proof of Theorem dfnot

Step	Hyp	Ref	Expression
1		pm2.21 100	. 2 |- (-. ph -> (ph -> F. ))
2		id 19	. . 3 |- (-. ph -> -. ph)
3		falim 1328	. . 3 |- ( F. -> -. ph)
4	2, 3	ja 153	. 2 |- ((ph -> F. ) -> -. ph)
5	1, 4	impbii 180	1 |- (-. ph <-> (ph -> F. ))

This proof depends on syntax axioms:  -. wn 3   -> wi 4   <-> wb 176   F. wfal 1317

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-tru 1319  df-fal 1320

This theorem is used by:  inegd  1333