Theorem 3eqtr4a 1954

Description: A chained equality inference, useful for converting to definitions. (The proof was shortened by Andrew Salmon, 25-May-2011.)

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.2	. . 3 |- (ph -> C = A)
2		3eqtr4a.1	. . 3 |- A = B
3	1, 2	syl6eq 1944	. 2 |- (ph -> C = B)
4		3eqtr4a.3	. 2 |- (ph -> D = B)
5	3, 4	eqtr4d 1928	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  uniintsn 3253  unizlim 3786  ordunisuc 3911  ordunisucOLD 3912  dmxpid 4179  fopabsnOLD 4816  1stval2 5030  2ndval2 5031  1st2val 5038  2nd2val 5039  oev2 5207  ecoprcom 5378  ecoprass 5379  ecoprdi 5380  xpmapenlem5 5594  unxpdomlem 5995  cardidm 6001  cardiun 6011  alephcard 6015  cardalephex 6034  cardcf 6059  eqnegi 6982  zeo 7411  sq01 7897  absexp 8119  facp1 8188  bcpasci 8221  binomi 8332  efexp 8634  sin01bndlem3 8735  infxpidmlem4 8824  alephadd 8851  grpsn 9340  ringsn 9490  ipid 9702  ipasslem1 9831  symggrpi 10205  pjclem2 11769  cvmdi 11896  rnxpid 14409  hmeogrp 14892  clsingemp 14961  idtrgrp 14978  1ded 15085  idsubfun 15206  heiborlem8 15962  pcoass 16085  iotain 16381  stb2xpl 16742  stb3xpl 16743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain