Theorem 3eqtr4a 1579

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

Syntax hints:   -> wi 3   = wceq 997

This theorem is referenced by:  ordunisuc 3146  unizlim 3170  dmsnop 3385  dmxpid 3390  fopabsn 3897  1stval2 4147  2ndval2 4148  oev2 4220  ecoprcom 4380  ecoprass 4381  ecoprdi 4382  xpmapenlem5 4565  unxpdomlem 4908  cardidm 4914  cardiun 4924  alephcard 4932  cardalephex 4951  cardcf 4976  eqnegi 5862  zeo 6284  sq01 6740  absexp 6958  facp1 7026  bcpasci 7059  binomi 7162  efexp 7462  sin01bndlem3 7561  infxpidmlem4 7647  alephadd 7674  grpsn 8208  ringsn 8247  ipid 8447  ipasslem1 8574  pjclem2 10208  cvmdi 10335  symggrpi 10491  hmeogrp 10632  1ded 10753

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain