Theorem mpbi 72

Description: Deduction from equality inference.

Hypotheses

Ref	Expression
mpbi.1	|- R |= A
mpbi.2	|- R |= [A = B]

Assertion

Ref	Expression
mpbi	|- R |= B

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.1	. 2 |- R |= A
2		weq 38	. . 3 |- = :(* -> (* -> *))
3	1	ax-cb2 30	. . 3 |- A:*
4		mpbi.2	. . . 4 |- R |= [A = B]
5	3, 4	eqtypi 69	. . 3 |- B:*
6	2, 3, 5, 4	dfov1 66	. 2 |- R |= (( = A)B)
7	1, 6	ax-eqmp 42	1 |- R |= B

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-eqmp 42

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  mpbir  77  eqtri  85  ax4g  139  ax4  140  cla4v  142  pm2.21  143  dfan2  144  mpd  146  notval2  149  notnot1  150  con2d  151  ecase  153  exlimdv2  156  exlimd  171  alnex  174  exnal1  175  exmid  186  notnot  187  ax3  192  ax11  201  ax13  203  ax14  204