Theorem 3eqtr4a 1532

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 1517	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  ordunisuc 3089  unizlim 3113  dmsnop 3328  dmxpid 3333  fopabsn 3840  1stval2 4089  2ndval2 4090  oev2 4162  ecoprcom 4319  ecoprass 4320  ecoprdi 4321  xpmapenlem5 4500  unxpdomlem 4843  cardidm 4849  cardiun 4859  alephcard 4867  cardalephex 4886  cardcf 4911  eqneg 5804  zeot 6199  sq01t 6651  absexpt 6868  facp1t 6936  bcpasc 6969  binom 7072  efexpt 7372  sin01bndlem3 7469  infxpidmlem4 7555  alephadd 7582  grpsn 8124  ringsn 8163  ipid 8363  ipasslem1 8490  pjclem2 10124  cvmd 10251  symggrpi 10406  hmeogrp 10538  1ded 10671

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain