Theorem syl5eq 2125

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eq.1	⊢ 𝐴 = 𝐵
syl5eq.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl5eq.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrd 2113	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  syl5req  2126  syl5eqr  2127  3eqtr3a  2137  3eqtr4g  2138  csbtt  2918  csbvarg  2933  csbie2g  2952  rabbi2dva  3174  csbprc  3289  disjssun  3307  disjpr2  3456  prprc2  3501  difprsn2  3526  opprc  3591  intsng  3670  riinm  3750  iinxsng  3751  rintm  3765  sucprc  4167  unisucg  4169  xpriindim  4492  relop  4504  dmxpm  4573  riinint  4611  resabs1  4658  resabs2  4659  resima2  4662  xpssres  4663  resopab2  4675  imasng  4710  ndmima  4722  xpdisj1  4767  xpdisj2  4768  djudisj  4770  resdisj  4771  rnxpm  4772  xpima1  4787  xpima2m  4788  dmsnsnsng  4818  rnsnopg  4819  rnpropg  4820  mptiniseg  4835  dfco2a  4841  relcoi1  4869  unixpm  4873  iotaval  4898  funtp  4972  fnun  5025  fnresdisj  5029  fnima  5037  fnimaeq0  5040  fcoi1  5090  f1orescnv  5162  foun  5165  resdif  5168  tz6.12-2  5189  fveu  5190  tz6.12-1  5221  fvun2  5261  fvopab3ig  5267  f1oresrab  5350  dfmptg  5363  ressnop0  5365  fvunsng  5378  fsnunfv  5384  fvpr1  5386  fvpr2  5387  fvpr1g  5388  fvpr2g  5389  fvtp1g  5390  fvtp2g  5391  fvtp3g  5392  fvtp2  5394  fvtp3  5395  f1oiso2  5486  riotaund  5522  ovprc  5560  resoprab2  5618  fnoprabg  5622  ovidig  5638  ovigg  5641  ov6g  5658  ovconst2  5672  offval2  5746  ot1stg  5799  ot2ndg  5800  ot3rdgg  5801  fmpt2co  5857  algrflemg  5871  tpostpos2  5903  rdgisuc1  5994  frec0g  6006  frecsuclem1  6010  frecsuclem2  6012  frecrdg  6015  oasuc  6067  oa1suc  6070  omsuc  6074  nnm1  6120  nnm2  6121  dfec2  6132  errn  6151  phplem2  6339  eqinfti  6433  infvalti  6435  infsnti  6443  1qec  6578  mulidnq  6579  addpinq1  6654  0idsr  6944  1idsr  6945  caucvgsrlemoffres  6976  caucvgsr  6978  mulresr  7006  pitonnlem2  7015  ax1rid  7043  axcnre  7047  negid  7355  subneg  7357  negneg  7358  dfinfre  8034  2times  8160  infrenegsupex  8682  rexneg  8897  fseq1p1m1  9111  fzosplitprm1  9243  intfracq  9322  frec2uz0d  9401  frec2uzrdg  9411  frecuzrdg0  9416  iseqval  9440  sqval  9534  iexpcyc  9579  binom3  9590  faclbnd  9668  faclbnd2  9669  bcn1  9685  shftlem  9704  shftuz  9705  shftidt  9721  reim0  9748  remullem  9758  resqrexlemf1  9894  resqrexlemcalc3  9902  absexpzap  9966  absimle  9970  amgm2  10004  minmax  10112  ialgr0  10426  ialgrp1  10428  eucialg  10441  ex-ceil  10564  qdencn  10785