Metamath Proof Explorer


Theorem reseq12i

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses reseqi.1 A = B
reseqi.2 C = D
Assertion reseq12i A C = B D

Proof

Step Hyp Ref Expression
1 reseqi.1 A = B
2 reseqi.2 C = D
3 1 reseq1i A C = B C
4 2 reseq2i B C = B D
5 3 4 eqtri A C = B D