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