Theorem tbw-negdf

Description: The definition of negation, in terms of -> and F. . (Contributed by Anthony Hart, 15-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	tbw-negdf	|- ( ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> -. ph ) -> F. ) ) -> F. )

Proof

Step	Hyp	Ref	Expression
1		pm2.21	|- ( -. ph -> ( ph -> F. ) )
2		ax-1	|- ( -. ph -> ( ( ph -> F. ) -> -. ph ) )
3		falim	|- ( F. -> ( ( ph -> F. ) -> -. ph ) )
4	2 3	ja	|- ( ( ph -> F. ) -> ( ( ph -> F. ) -> -. ph ) )
5	4	pm2.43i	|- ( ( ph -> F. ) -> -. ph )
6	1 5	impbii	|- ( -. ph <-> ( ph -> F. ) )
7		tbw-bijust	|- ( ( -. ph <-> ( ph -> F. ) ) <-> ( ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> -. ph ) -> F. ) ) -> F. ) )
8	6 7	mpbi	|- ( ( ( -. ph -> ( ph -> F. ) ) -> ( ( ( ph -> F. ) -> -. ph ) -> F. ) ) -> F. )