Theorem mpbirx 53

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

Hypotheses

Ref	Expression
mpbirx.1	⊢ B:∗
mpbirx.2	⊢ R⊧A
mpbirx.3	⊢ R⊧(( = B)A)

Assertion

Ref	Expression
mpbirx	⊢ R⊧B

Proof of Theorem mpbirx

Step	Hyp	Ref	Expression
1		mpbirx.2	. 2 ⊢ R⊧A
2		mpbirx.1	. . 3 ⊢ B:∗
3	1	ax-cb2 30	. . 3 ⊢ A:∗
4		mpbirx.3	. . 3 ⊢ R⊧(( = B)A)
5	2, 3, 4	eqcomx 52	. 2 ⊢ R⊧(( = A)B)
6	1, 5	ax-eqmp 45	1 ⊢ R⊧B

Syntax hints:  ∗hb 3  kc 5   = ke 7  ⊧wffMMJ2 11  wffMMJ2t 12

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

This theorem is referenced by:  dfov2  75