Theorem mpbi 82

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

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 41	. . 3 ⊢ = :(∗ → (∗ → ∗))
3	1	ax-cb2 30	. . 3 ⊢ A:∗
4		mpbi.2	. . . 4 ⊢ R⊧[A = B]
5	3, 4	eqtypi 78	. . 3 ⊢ B:∗
6	2, 3, 5, 4	dfov1 74	. 2 ⊢ R⊧(( = A)B)
7	1, 6	ax-eqmp 45	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-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