Theorem eqtru 86

Description: If a statement is provable, then it is equivalent to truth. (Contributed by Mario Carneiro, 8-Oct-2014.)

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 43	. . 3 |- T.:*
3	1, 2	adantr 55	. 2 |- (R, T.) |= A
4	1	ax-cb1 29	. . . 4 |- R:*
5	1	ax-cb2 30	. . . 4 |- A:*
6	4, 5	wct 48	. . 3 |- (R, A):*
7		tru 44	. . 3 |- T. |= T.
8	6, 7	a1i 28	. 2 |- (R, A) |= T.
9	3, 8	ded 84	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-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wov 71

This theorem depends on definitions:  df-ov 73

This theorem is referenced by:  hbth  109  alrimiv  151  dfan2  154  olc  164  orc  165  alrimi  182  exmid  199  ax9  212