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

Theorem mpbi 82
Description: Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
Hypotheses
Ref Expression
mpbi.1 RA
mpbi.2 R⊧[A = B]
Assertion
Ref Expression
mpbi RB

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.1 . 2 RA
2 weq 41 . . 3 = :(∗ → (∗ → ∗))
31ax-cb2 30 . . 3 A:∗
4 mpbi.2 . . . 4 R⊧[A = B]
53, 4eqtypi 78 . . 3 B:∗
62, 3, 5, 4dfov1 74 . 2 R⊧(( = A)B)
71, 6ax-eqmp 45 1 RB
Colors of variables: type var term
Syntax hints:  hb 3   = ke 7  [kbr 9  wffMMJ2 11
This theorem was proved from axioms:  ax-syl 15  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-eqmp 45  ax-eqtypi 77
This theorem depends on definitions:  df-ov 73
This theorem is referenced by:  mpbir  87  eqtri  95  ax4g  149  ax4  150  cla4v  152  pm2.21  153  dfan2  154  mpd  156  notval2  159  notnot1  160  con2d  161  ecase  163  exlimdv2  166  exlimd  183  alnex  186  exnal1  187  exmid  199  notnot  200  ax3  205  ax11  214  ax13  216  ax14  217
  Copyright terms: Public domain W3C validator