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

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 RA
Assertion
Ref Expression
eqtru R⊧[⊤ = A]

Proof of Theorem eqtru
StepHypRef Expression
1 eqtru.1 . . 3 RA
2 wtru 43 . . 3 ⊤:∗
31, 2adantr 55 . 2 (R, ⊤)⊧A
41ax-cb1 29 . . . 4 R:∗
51ax-cb2 30 . . . 4 A:∗
64, 5wct 48 . . 3 (R, A):∗
7 tru 44 . . 3 ⊤⊧⊤
86, 7a1i 28 . 2 (R, A)⊧⊤
93, 8ded 84 1 R⊧[⊤ = A]
 Colors of variables: type var term 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
 Copyright terms: Public domain W3C validator