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⊧[⊤ = A]

Proof of Theorem eqtru

Step	Hyp	Ref	Expression
1		eqtru.1	. . 3 ⊢ R⊧A
2		wtru 43	. . 3 ⊢ ⊤:∗
3	1, 2	adantr 55	. 2 ⊢ (R, ⊤)⊧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 ⊢ ⊤⊧⊤
8	6, 7	a1i 28	. 2 ⊢ (R, A)⊧⊤
9	3, 8	ded 84	1 ⊢ R⊧[⊤ = A]

Syntax hints:   = ke 7  ⊤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