Metamath Proof Explorer


Theorem oteq1d

Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypothesis oteq1d.1 φA=B
Assertion oteq1d φACD=BCD

Proof

Step Hyp Ref Expression
1 oteq1d.1 φA=B
2 oteq1 A=BACD=BCD
3 1 2 syl φACD=BCD