eqtru - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > eqtru		Unicode version

Theorem eqtru 76

Description: If a statement is provable, then it is equivalent to truth.

**Hypothesis**
Ref	Expression
eqtru.1

**Assertion**
Ref	Expression
eqtru

**Proof of Theorem eqtru**
Step	Hyp	Ref	Expression
1		eqtru.1	. . 3
2		wtru 40	. . 3
3	1, 2	adantr 50	. 2
4	1	ax-cb1 29	. . . 4
5	1	ax-cb2 30	. . . 4
6	4, 5	wct 44	. . 3
7		tru 41	. . 3
8	6, 7	a1i 28	. 2
9	3, 8	ded 74	1

Colors of variables: type var term

Syntax hints:

ke 7

kt 8

kbr 9 kct 10

This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-simpl 20 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ded 43 ax-ceq 46

This theorem depends on definitions: df-ov 65

This theorem is referenced by: hbth 99 alrimiv 141 dfan2 144 olc 154 orc 155 alrimi 170 exmid 186 ax9 199