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

Proof of Theorem eqtru

Step	Hyp	Ref	Expression
1		eqtru.1	. . 3 ⊢ R⊧A
2		wtru 40	. . 3 ⊢ ⊤:∗
3	1, 2	adantr 50	. 2 ⊢ (R, ⊤)⊧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 ⊢ ⊤⊧⊤
8	6, 7	a1i 28	. 2 ⊢ (R, A)⊧⊤
9	3, 8	ded 74	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-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