This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Classes Class equality 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 ⊢ ( 𝜑 → 𝐶 = 𝐷 )