Theorem mpbir 87

Description: Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Hypotheses

Ref	Expression
mpbir.1	⊢ R⊧A
mpbir.2	⊢ R⊧[B = A]

Assertion

Ref	Expression
mpbir	⊢ R⊧B

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.1	. 2 ⊢ R⊧A
2	1	ax-cb2 30	. . . 4 ⊢ A:∗
3		mpbir.2	. . . 4 ⊢ R⊧[B = A]
4	2, 3	eqtypri 81	. . 3 ⊢ B:∗
5	4, 3	eqcomi 79	. 2 ⊢ R⊧[A = B]
6	1, 5	mpbi 82	1 ⊢ R⊧B

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