Theorem 3eqtr3g 2827

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3g.2	⊢ 𝐴 = 𝐶
3eqtr3g.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 ⊢ 𝐴 = 𝐶
2		3eqtr3g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr3id 2818	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2820	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  csbnest1g  4401  disjdif2  4444  diftpsn3  4772  tppreqb  4775  xpid11  5923  cores2  6262  funcoeqres  6853  fvunsn  7178  caovmo  7648  dftpos2  8239  fvmpocurryd  8267  tfrlem16  8380  oev2  8508  domss2  9124  enp1ilem  9238  fipreima  9315  dfac5lem3  10109  fpwwe2lem12  10627  canthwelem  10635  canthp1lem2  10638  reclem3pr  11034  mulcmpblnrlem  11055  1idsr  11083  mulgt0sr  11090  mul02lem2  11387  ine0  11649  lo1eq  15619  rlimeq  15620  sumeq2ii  15744  fsumf1o  15774  sumss  15775  fsumss  15776  fsumadd  15791  fsumcom2  15825  fsum0diag2  15834  fsummulc2  15835  fsumrelem  15859  isumshft  15893  mertenslem1  15938  prodeq2ii  15965  fprodf1o  16000  prodss  16001  fprodss  16002  fprodmul  16014  fproddiv  16015  fprodcom2  16038  fprodmodd  16051  fprodefsum  16149  bitsinv1  16500  bitsinvp1  16507  4sqlem10  17007  setsnid  17268  topnpropd  17489  xpsff1o  17621  homfeqbas  17752  comfffval2  17757  comfeq  17762  oppchomfpropd  17782  isssc  17877  funcpropd  17959  hofpropd  18323  eqglact  19247  symgvalstruct  19467  lsmmod2  19746  vrgpinv  19839  frgpnabllem1  19943  frgpnabllem2  19944  gsum2dlem2  20041  dprddisj2  20111  ablfac1eulem  20144  ringpropd  20371  crngpropd  20372  mulgass3  20435  rngidpropd  20497  invrpropd  20500  isrhm2d  20569  subrngpropd  20653  subrgpropd  20693  rhmpropd  20694  lss0v  21115  lidlrsppropd  21352  ressmpladd  22148  ressmplmul  22149  ressmplvsca  22150  eqcoe1ply1eq  22428  resstopn  23312  lecldbas  23345  isref  23635  txhaus  23773  qustgplem  24247  tuslem  24392  imasdsf1olem  24499  metustsym  24681  reconnlem1  24953  voliunlem1  25678  ismbf3d  25782  i1fima  25806  i1fd  25809  itgfsum  25955  dvmptc  26086  dvmptfsum  26103  dvfsumle  26149  dvfsumlem2  26155  itgsubst  26177  atantayl2  27069  chtdif  27288  ppidif  27293  fsumdvdsmul  27325  onleft  28419  oncutlt  28423  pythi  31143  hvsubeq0i  31356  hvaddcani  31358  cmcmlem  31884  pj11i  32004  hosubeq0i  32119  riesz3i  32355  pjclem1  32488  pjclem3  32490  st0  32542  chirredi  32687  mdsymi  32704  difeq  32805  unidifsnne  32823  1nei  33023  subrgchr  33497  ressply1evls1  33800  srapwov  33924  locfinref  34176  esumpfinvallem  34409  esum2dlem  34427  carsgclctun  34656  ballotlemgun  34860  cvmliftmolem1  35706  cvmlift3lem6  35749  msubff1  35981  isfne  36773  isfne4  36774  isfne4b  36775  bj-1uplth  37566  bj-2uplth  37580  matunitlindflem1  38190  ptrest  38193  poimirlem3  38197  poimirlem4  38198  poimirlem8  38202  poimirlem15  38209  mblfinlem2  38232  voliunnfl  38238  cdlemg47  41435  ltrnco4  41438  sn-1ne2  42957  sn-00idlem3  43086  sn-0tie0  43150  sn-inelr  43186  eldioph2  43420  binomcxplemdvbinom  44990  binomcxplemnotnn0  44993  compne  45077  rnfdmpr  47942  cycl3grtri  48636