Theorem eqtru 76

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

Hypothesis

Ref	Expression
eqtru.1	|- R |= A

Assertion

Ref	Expression
eqtru	|- R |= [T. = A]

Proof of Theorem eqtru

Step	Hyp	Ref	Expression
1		eqtru.1	. . 3 |- R |= A
2		wtru 40	. . 3 |- T.:*
3	1, 2	adantr 50	. 2 |- (R, T.) |= A
4	1	ax-cb1 29	. . . 4 |- R:*
5	1	ax-cb2 30	. . . 4 |- A:*
6	4, 5	wct 44	. . 3 |- (R, A):*
7		tru 41	. . 3 |- T. |= T.
8	6, 7	a1i 28	. 2 |- (R, A) |= T.
9	3, 8	ded 74	1 |- R |= [T. = A]

Syntax hints:   = ke 7  T.kt 8  [kbr 9  kct 10   |= wffMMJ2 11

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