Theorem 3eqtr4a 1530

Description: A chained equality inference, useful for converting to definitions.

Hypotheses

Ref	Expression
3eqtr4a.1	|- A = B
3eqtr4a.2	|- (ph -> C = A)
3eqtr4a.3	|- (ph -> D = B)

Assertion

Ref	Expression
3eqtr4a	|- (ph -> C = D)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.1	. . 3 |- A = B
2	1	a1i 8	. 2 |- (ph -> A = B)
3		3eqtr4a.2	. 2 |- (ph -> C = A)
4		3eqtr4a.3	. 2 |- (ph -> D = B)
5	2, 3, 4	3eqtr4d 1515	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  ordunisuc 3085  unizlim 3109  dmsnop 3324  dmxpid 3329  fopabsn 3835  1stval2 4082  2ndval2 4083  oev2 4155  ecoprcom 4312  ecoprass 4313  ecoprdi 4314  xpmapenlem5 4489  unxpdomlem 4826  cardidm 4832  cardiun 4842  alephcard 4850  cardalephex 4869  cardcf 4894  eqneg 5770  zeot 6156  sq01t 6596  absexpt 6818  facp1t 6888  bcpasc 6922  binom 7025  efexpt 7331  sin01bndlem3 7428  infxpidmlem4 7515  alephadd 7542  grpsn 8088  ringsn 8127  ipid 8325  ipasslem1 8449  pjclem2 10080  cvmd 10207  symggrpi 10362  hmeogrp 10484  1ded 10587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468

Copyright terms: Public domain