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

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

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.1 . 2 RA
21ax-cb2 30 . . . 4 A:∗
3 mpbir.2 . . . 4 R⊧[B = A]
42, 3eqtypri 81 . . 3 B:∗
54, 3eqcomi 79 . 2 R⊧[A = B]
61, 5mpbi 82 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-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80 This theorem depends on definitions:  df-ov 73 This theorem is referenced by:  ax4g  149  alrimiv  151  dfan2  154  mpd  156  ex  158  notnot1  160  con2d  161  olc  164  orc  165  ax4e  168  cla4ev  169  19.8a  170  alrimi  182  alnex  186  exmid  199  ax9  212  ax10  213  ax11  214  axrep  220
 Copyright terms: Public domain W3C validator