Theorem syl5eq 2209

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 2197	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157

This theorem is referenced by:  eqtr2id  2210  eqtr3id  2211  3eqtr3a  2221  3eqtr4g  2222  csbtt  3052  csbvarg  3068  csbie2g  3090  rabbi2dva  3325  csbprc  3449  disjssun  3467  disjpr2  3634  prprc2  3679  difprsn2  3707  opprc  3773  intsng  3852  riinm  3932  iinxsng  3933  iunxprg  3940  rintm  3952  sucprc  4384  unisucg  4386  xpriindim  4736  relop  4748  dmxpm  4818  riinint  4859  resabs1  4907  resabs2  4909  resima2  4912  xpssres  4913  resopab2  4925  imasng  4963  ndmima  4975  xpdisj1  5022  xpdisj2  5023  djudisj  5025  resdisj  5026  rnxpm  5027  xpima1  5044  xpima2m  5045  dmsnsnsng  5075  rnsnopg  5076  rnpropg  5077  mptiniseg  5092  dfco2a  5098  relcoi1  5129  unixpm  5133  iotaval  5158  funtp  5235  fnun  5288  fnresdisj  5292  fnima  5300  fnimaeq0  5303  fcoi1  5362  f1orescnv  5442  foun  5445  resdif  5448  tz6.12-2  5471  fveu  5472  tz6.12-1  5507  fvun2  5547  fvopab3ig  5554  f1oresrab  5644  dfmptg  5658  ressnop0  5660  fvunsng  5673  fnsnsplitss  5678  fsnunfv  5680  fvpr1  5683  fvpr2  5684  fvpr1g  5685  fvpr2g  5686  fvtp1g  5687  fvtp2g  5688  fvtp3g  5689  fvtp2  5691  fvtp3  5692  f1oiso2  5789  riotaund  5826  ovprc  5868  resoprab2  5930  fnoprabg  5934  ovidig  5950  ovigg  5953  ov6g  5970  ovconst2  5984  offval2  6059  ot1stg  6112  ot2ndg  6113  ot3rdgg  6114  fmpoco  6175  algrflemg  6189  tpostpos2  6224  rdgisuc1  6343  frec0g  6356  frecsuclem  6365  frecrdg  6367  oasuc  6423  oa1suc  6426  omsuc  6431  nnm1  6483  nnm2  6484  dfec2  6495  errn  6514  ixpsnval  6658  ixpintm  6682  mapen  6803  xpmapenlem  6806  phplem2  6810  undifdc  6880  fisseneq  6888  ssfirab  6890  eqinfti  6976  infvalti  6978  infsnti  6986  casef  7044  caseinl  7047  caseinr  7048  djudom  7049  ctssdccl  7067  exmidfodomrlemim  7148  1qec  7320  mulidnq  7321  addpinq1  7396  suplocexprlem2b  7646  suplocexprlemlub  7656  0idsr  7699  1idsr  7700  caucvgsrlemoffres  7732  caucvgsr  7734  mulresr  7770  pitonnlem2  7779  ax1rid  7809  axcnre  7813  negid  8136  subneg  8138  negneg  8139  dfinfre  8842  2times  8976  infrenegsupex  9523  rexneg  9757  xaddpnf2  9774  xaddmnf1  9775  xaddmnf2  9776  fseq1p1m1  10019  fzosplitprm1  10159  intfracq  10245  frec2uz0d  10324  frec2uzrdg  10334  frecuzrdg0  10338  frecuzrdgg  10341  frecuzrdg0t  10347  seq3val  10383  seqvalcd  10384  iseqf1olemjpcl  10420  iseqf1olemqpcl  10421  iseqf1olemfvp  10422  seq3f1olemqsum  10425  sqval  10503  iexpcyc  10549  binom3  10561  faclbnd  10643  faclbnd2  10644  bcn1  10660  hashinfom  10680  hashennn  10682  hashxp  10728  shftlem  10744  shftuz  10745  shftidt  10761  reim0  10789  remullem  10799  resqrexlemf1  10936  resqrexlemcalc3  10944  absexpzap  11008  absimle  11012  amgm2  11046  minmax  11157  mingeb  11169  2zinfmin  11170  xrmaxiflemval  11177  xrmaxadd  11188  infxrnegsupex  11190  xrminmax  11192  summodc  11310  fsum3  11314  sumsnf  11336  sumsns  11342  isumclim3  11350  isumge0  11357  fsump1i  11360  fsum2dlemstep  11361  fisumcom2  11365  fsumshftm  11372  fsumconst  11381  fsumiun  11404  hashrabrex  11408  hashuni  11409  binom11  11413  isumsplit  11418  geo2sum  11441  mertensabs  11464  prodmodc  11505  fprodseq  11510  prodsnf  11519  prodsns  11530  fprodconst  11547  fprod2dlemstep  11549  fprodcom2fi  11553  efgt1p2  11622  efgt1p  11623  resinval  11642  recosval  11643  cosadd  11664  ef01bndlem  11683  eirraplem  11703  ialgr0  11955  algrp1  11957  eucalg  11970  phiprmpw  12131  phiprm  12132  prmdiv  12144  pythagtriplem12  12184  pythagtriplem14  12186  pythagtriplem16  12188  pceu  12204  pcfac  12257  ennnfonelem0  12275  ennnfonelemfun  12287  ennnfonelemf1  12288  ennnfonelemrn  12289  ctinfomlemom  12297  nninfdclemp1  12322  ndxid  12355  setsfun0  12367  setsresg  12369  setscom  12371  strslfv2d  12373  ressid2  12390  ressval2  12391  tgidm  12615  tgrest  12710  ssidcn  12751  txcnmpt  12814  txcn  12816  blres  12975  mopnval  12983  remetdval  13080  divccncfap  13118  cncfmet  13120  cncfcncntop  13121  cnplimcim  13177  cnplimclemr  13179  limccnpcntop  13185  limccnp2cntop  13187  dvexp  13216  sin0pilem1  13243  pilem3  13245  ef2kpi  13268  sin2pim  13275  cos2pim  13276  sinmpi  13277  cosmpi  13278  sinppi  13279  cosppi  13280  sinhalfpip  13282  sinhalfpim  13283  coshalfpip  13284  coshalfpim  13285  tangtx  13300  1cxp  13362  ecxp  13363  rplogb1  13407  rpelogb  13408  binom4  13438  ex-ceil  13444  qdencn  13740  cvgcmp2nlemabs  13745  trilpolemlt1  13754  nconstwlpolem0  13775