Metamath Proof Explorer
Description: A chained equality inference for a binary relation. (Contributed by NM, 11Oct1999)


Ref 
Expression 

Hypotheses 
eqbrtrid.1 
$${\u22a2}{A}={B}$$ 


eqbrtrid.2 
$${\u22a2}{\phi}\to {B}{R}{C}$$ 

Assertion 
eqbrtrid 
$${\u22a2}{\phi}\to {A}{R}{C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqbrtrid.1 
$${\u22a2}{A}={B}$$ 
2 

eqbrtrid.2 
$${\u22a2}{\phi}\to {B}{R}{C}$$ 
3 

eqid 
$${\u22a2}{C}={C}$$ 
4 
2 1 3

3brtr4g 
$${\u22a2}{\phi}\to {A}{R}{C}$$ 