Theorem mpbir 77

Description: Deduction from equality inference.

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 71	. . 3 |- B:*
5	4, 3	eqcomi 70	. 2 |- R |= [A = B]
6	1, 5	mpbi 72	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-refl 39  ax-eqmp 42  ax-ceq 46

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  ax4g  139  alrimiv  141  dfan2  144  mpd  146  ex  148  notnot1  150  con2d  151  olc  154  orc  155  ax4e  158  cla4ev  159  19.8a  160  alrimi  170  alnex  174  exmid  186  ax9  199  ax10  200  ax11  201  axrep  207