Metamath Proof Explorer


Theorem 3eqtr4a

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Hypotheses 3eqtr4a.1 𝐴 = 𝐵
3eqtr4a.2 ( 𝜑𝐶 = 𝐴 )
3eqtr4a.3 ( 𝜑𝐷 = 𝐵 )
Assertion 3eqtr4a ( 𝜑𝐶 = 𝐷 )

Proof

Step Hyp Ref Expression
1 3eqtr4a.1 𝐴 = 𝐵
2 3eqtr4a.2 ( 𝜑𝐶 = 𝐴 )
3 3eqtr4a.3 ( 𝜑𝐷 = 𝐵 )
4 2 1 eqtrdi ( 𝜑𝐶 = 𝐵 )
5 4 3 eqtr4d ( 𝜑𝐶 = 𝐷 )