Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Classes
Class equality
3eqtr4a
Metamath Proof Explorer
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
$${\u22a2}{A}={B}$$
3eqtr4a.2
$${\u22a2}{\phi}\to {C}={A}$$
3eqtr4a.3
$${\u22a2}{\phi}\to {D}={B}$$
Assertion
3eqtr4a
$${\u22a2}{\phi}\to {C}={D}$$

Proof
Step
Hyp
Ref
Expression
1
3eqtr4a.1
$${\u22a2}{A}={B}$$
2
3eqtr4a.2
$${\u22a2}{\phi}\to {C}={A}$$
3
3eqtr4a.3
$${\u22a2}{\phi}\to {D}={B}$$
4
2 1
eqtrdi
$${\u22a2}{\phi}\to {C}={B}$$
5
4 3
eqtr4d
$${\u22a2}{\phi}\to {C}={D}$$