dff2 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > dff2		Unicode version

Theorem dff2 100

Description: Alternate defintion of "false".

**Assertion**
Ref	Expression
dff2

**Proof of Theorem dff2**
Step	Hyp	Ref	Expression
1		df-f 42	. 2
2		df-t 41	. . 3
3	2	ax-r4 37	. 2
4	1, 3	ax-r2 36	1

Colors of variables: term

Syntax hints:

wb 1

wn 4

wo 6

wt 8

wf 9

This theorem was proved from axioms: ax-r2 36 ax-r4 37

This theorem depends on definitions: df-t 41 df-f 42

This theorem is referenced by: dff 101 or0 102