HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  mpbirx Unicode version

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
StepHypRef Expression
1 mpbirx.2 . 2 |- R |= A
2 mpbirx.1 . . 3 |- B:*
31ax-cb2 30 . . 3 |- A:*
4 mpbirx.3 . . 3 |- R |= (( = B)A)
52, 3, 4eqcomx 52 . 2 |- R |= (( = A)B)
61, 5ax-eqmp 45 1 |- R |= B
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator