Theorem eqtr4i 2771

Description: An equality transitivity inference. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	⊢ 𝐴 = 𝐵
eqtr4i.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2749	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2768	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  3eqtr2i  2774  3eqtr2ri  2775  3eqtr4i  2778  3eqtr4ri  2779  rabab  3520  cbvralcsf  3966  cbvrabcsf  3969  dfin5  3984  dfdif2  3985  uneqin  4308  notabw  4332  unrab  4334  inrab  4335  inrab2  4336  difrab  4337  dfrab3ss  4342  rabun2  4343  dfnul2  4355  difid  4398  rabxm  4413  elnelun  4416  abf  4429  difdifdir  4515  dfif3  4562  dfif5  4564  rabsnif  4748  tpidm  4783  ssunpr  4859  sstp  4861  opidg  4916  dfint2  4972  iunrab  5075  uniiun  5081  intiin  5082  iunid  5083  0iin  5087  mptv  5282  dfepfr  5684  epfrc  5685  xpundi  5768  xpundir  5769  csbcnv  5908  resiun2  6030  resopab  6063  mptresid  6080  dffr3  6129  dfse2  6130  cnvun  6174  imaundir  6182  imainrect  6212  cnvcnv2  6224  cnvrescnv  6226  cnvcnvres  6236  dmtpop  6249  rnsnopg  6252  resdifdi  6267  rnco2  6284  dmco  6285  co01  6292  unidmrn  6310  dfdm2  6312  predidm  6358  tz6.26OLD  6380  dfmpt3  6714  mptun  6726  funcocnv2  6887  dffv2  7017  fnasrn  7179  fpr  7188  fmptap  7204  rnmptc  7244  riotav  7409  dmoprab  7552  rnoprab2  7555  mpov  7562  mpomptx  7563  abrexex2g  8005  1stval2  8047  2ndval2  8048  fo1st  8050  fo2nd  8051  xp2  8067  dfoprab4f  8097  offval22  8129  fmpoco  8136  fimaproj  8176  tposmpo  8304  tposconst  8305  recsfval  8437  rdgsucmpt2  8486  frsucmpt2  8496  df2o3  8530  o1p1e2  8596  o2p2e4  8597  oarec  8618  omopthlem2  8716  ecqs  8839  qliftf  8863  erovlem  8871  fset0  8912  mapsnf1o3  8953  ixp0x  8984  omf1o  9141  xpf1o  9205  mapunen  9212  enp1ilem  9340  pwfiOLD  9417  marypha1lem  9502  marypha2lem4  9507  dfoi  9580  infeq5i  9705  oemapso  9751  cantnflem1  9758  rankelop  9943  leweon  10080  r0weon  10081  kmlem11  10230  dju1dif  10242  ackbij1lem16  10303  cf0  10320  cfsmolem  10339  alephsuc3  10649  fpwwe  10715  canthp1lem1  10721  wuncval2  10816  prlem936  11116  m1p1sr  11161  m1m1sr  11162  dfcnqs  11211  ssxr  11359  mul02lem2  11467  addrid  11470  2p2e4  12428  3p2e5  12444  3p3e6  12445  4p2e6  12446  4p3e7  12447  4p4e8  12448  5p2e7  12449  5p3e8  12450  5p4e9  12451  6p2e8  12452  6p3e9  12453  7p2e9  12454  nnzrab  12671  nn0zrab  12672  dec0u  12779  dec0h  12780  decsuc  12789  decsucc  12799  numma  12802  decma  12809  decmac  12810  decma2c  12811  decadd  12812  decaddc  12813  decmul1c  12823  decmul2c  12824  5p5e10  12829  6p4e10  12830  7p3e10  12833  8p2e10  12838  5t5e25  12861  6t6e36  12866  8t6e48  12877  nn0uz  12945  nnuz  12946  xaddcom  13302  x2times  13361  ioomax  13482  iccmax  13483  ioopos  13484  ioorp  13485  prunioo  13541  fseq1p1m1  13658  fzo13pr  13800  fzo0to2pr  13801  fzo0to3tp  13802  om2uzrdg  14007  fzennn  14019  irec  14250  sq10e99m1  14314  facnn  14324  fac0  14325  faclbnd2  14340  faclbnd4lem1  14342  hashfun  14486  hashbclem  14501  hashf1lem1  14504  hashf1lem2  14505  fz1isolem  14510  swrdccatin1  14773  swrdccat3blem  14787  s1co  14882  s2eq2s1eq  14985  s3eqs2s1eq  14987  ofs2  15020  dfid5  15076  dfid6  15077  fsumrev2  15830  fsumparts  15854  fsumiun  15869  isumnn0nn  15890  harmonic  15907  fprod2d  16029  bpoly2  16105  bpoly3  16106  bpoly4  16107  ege2le3  16138  cos1bnd  16235  efieq1re  16247  eirrlem  16252  qnnen  16261  cpnnen  16277  ruclem6  16283  3dvds  16379  pwp1fsum  16439  m1bits  16486  nn0expgcd  16611  algrp1  16621  phiprmpw  16823  prmreclem4  16966  4sqlem11  17002  4sqlem19  17010  dec5dvds  17111  decsplit1  17129  5prm  17156  7prm  17158  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  strle1  17205  grpbasex  17350  grpplusgx  17351  quslem  17603  xpsrnbas  17631  acsfn1  17719  acsfn2  17721  comfffval2  17759  dfinito2  18070  dftermo2  18071  xpchomfval  18248  xpccofval  18251  1stfval  18260  2ndfval  18263  oduleg  18360  ismgmid  18703  efmndbas  18906  smndex2dnrinv  18950  grpinvfvi  19022  gaorb  19347  elcntr  19370  cntri  19372  cntrsubgnsg  19383  cntrnsg  19384  setsplusg  19390  oppglemOLD  19391  oppgcntr  19408  gsumwrev  19409  symgressbas  19423  symgplusg  19424  symgvalstruct  19438  symgvalstructOLD  19439  symgga  19449  cayleylem1  19454  psgnunilem2  19537  efgval2  19766  efgredlemc  19787  efgcpbllema  19796  frgpnabllem1  19915  gsumzaddlem  19963  mgplemOLD  20166  opprlem  20365  opprlemOLD  20366  oppr0  20375  opprneg  20377  rmodislmod  20950  rmodislmodOLD  20951  rlmscaf  21237  xrsds  21450  gsumfsum  21475  zringunit  21500  pzriprng1  21532  cnmsgngrp  21620  psgnfix2  21640  relt  21656  ocv0  21718  thlle  21739  thlleOLD  21740  thlleval  21741  dsmmval2  21779  frlmip  21821  mplbas  22033  mplplusg  22050  mplmulr  22051  mplvsca2  22057  ressmplbas2  22068  ltbwe  22085  evlslem4  22123  psdmul  22193  psr1bas2  22212  ply1bas  22217  ply1basOLD  22218  ply1assa  22222  psr1plusg  22243  psr1vsca  22244  psr1mulr  22245  ply1plusg  22246  ply1vsca  22247  ply1mulr  22248  ply1mpl0  22279  ply1mpl1  22281  coe1mul  22294  matgsum  22464  smadiadetglem1  22698  indistpsx  23038  iuncld  23074  tgrest  23188  resstopn  23215  leordtval2  23241  xkouni  23628  ptclsg  23644  ptuncnv  23836  ptunhmeo  23837  alexsubALTlem4  24079  tsmsf1o  24174  ucnimalem  24310  ressxms  24559  uniretop  24804  cnfldtopn  24823  xrtgioo  24847  zcld  24854  icccmp  24866  xrge0gsumle  24874  xrge0tsms  24875  metnrmlem3  24902  fsum2cn  24914  cnmpopc  24974  oprpiece1res1  25001  oprpiece1res2  25002  evth  25010  evth2  25011  om1opn  25088  pi1xfrf  25105  pi1xfrcnv  25109  pi1cof  25111  clsocv  25303  cncmet  25375  cnflduss  25409  rrxprds  25442  ehlbase  25468  ismbl  25580  shftmbl  25592  ioorinv  25630  itg1addlem4  25753  itg1addlem4OLD  25754  itg2cnlem1  25816  itg0  25835  itgss3  25870  ditgneg  25912  limcdif  25931  limciun  25949  dvexp  26011  dvef  26038  dvcnvrelem2  26077  ftc1  26103  aannenlem2  26389  dvradcnv  26482  pserdvlem2  26490  reefgim  26512  cospi  26532  sincos6thpi  26576  tanregt0  26599  dflog2  26620  logfac  26661  dvlog  26711  cxpexp  26728  cxpmul2  26749  cxpsqrt  26763  dvsqrt  26802  dvcnsqrt  26804  cxpcn2  26807  isosctrlem2  26880  1cubrlem  26902  1cubr  26903  quart1lem  26916  atancj  26971  atanlogaddlem  26974  atansopn  26993  leibpilem2  27002  log2cnv  27005  log2ublem3  27009  birthdaylem1  27012  birthdaylem2  27013  birthday  27015  dfarea  27021  lgamgulmlem5  27094  lgambdd  27098  ftalem3  27136  basellem2  27143  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  ppi2  27231  ppi3  27232  ppiub  27266  chtub  27274  bclbnd  27342  bposlem8  27353  lgsdilem  27386  lgsdir2lem2  27388  lgsquadlem2  27443  lgsquad2lem2  27447  2lgsoddprmlem3c  27474  rplogsum  27589  mulog2sumlem2  27597  pnt2  27675  bdayfo  27740  bday0s  27891  bday1s  27894  old1  27932  addsasslem2  28055  negsbdaylem  28106  muls01  28156  abssnid  28285  1p1e2s  28418  n0seo  28423  nohalf  28425  zs12bday  28442  istrkg2ld  28486  axsegconlem9  28958  ax5seglem7  28968  iedgedg  29085  uspgrf1oedg  29208  nbgrcl  29370  nbgrnvtx0  29374  rusgrprc  29626  pthsfval  29757  wlkiswwlks2lem4  29905  wlkiswwlks2lem5  29906  clwwlkvbij  30145  konigsbergumgr  30283  ex-pw  30461  ex-xp  30468  ex-rn  30472  nvvop  30641  nvm  30673  cnims  30725  ip0i  30857  ip1ilem  30858  ipdirilem  30861  ipasslem10  30871  h2hva  31006  h2hsm  31007  h2hvs  31009  axhfvadd-zf  31014  axhvcom-zf  31015  axhvass-zf  31016  axhv0cl-zf  31017  axhvaddid-zf  31018  axhfvmul-zf  31019  axhvmulid-zf  31020  axhvmulass-zf  31021  axhvdistr1-zf  31022  axhvdistr2-zf  31023  axhvmul0-zf  31024  axhfi-zf  31025  axhis1-zf  31026  axhis2-zf  31027  axhis3-zf  31028  axhis4-zf  31029  axhcompl-zf  31030  normlem0  31141  normlem1  31142  normlem2  31143  normlem4  31145  normlem9  31150  bcseqi  31152  dfhnorm2  31154  norm3difi  31179  normpari  31186  normpar2i  31188  polid2i  31189  polidi  31190  hhba  31199  hhims  31204  hhims2  31205  hhsssh  31301  hhssims  31306  hhssims2  31307  shsval3i  31420  dfch2  31439  cmcm2i  31625  fh2  31651  qlaxr3i  31668  spansnji  31678  pjcji  31716  ho0val  31782  df0op2  31784  hosd1i  31854  hosd2i  31855  eigorthi  31869  hhlnoi  31932  hhnmoi  31933  hhbloi  31934  bra0  31982  nmop0  32018  nmfn0  32019  lnopeq0lem1  32037  lnopunilem1  32042  lnophmlem2  32049  nmopcoadji  32133  pjhmopidm  32215  cvmdi  32356  cdj3lem3  32470  cdj3lem3b  32472  abrexdomjm  32535  uniin1  32574  uniin2  32575  iundifdifd  32584  iundifdif  32585  mpomptxf  32695  df1stres  32715  df2ndres  32716  intimafv  32722  fcobijfs  32737  resf1o  32744  fpwrelmapffslem  32746  dpval3  32858  dp3mul10  32862  dpadd2  32874  dpmul4  32878  ccatws1f1o  32918  chnub  32984  xrslt  32990  xrsclat  32994  xrge0tsmsd  33041  gsumle  33074  cycpmco2lem7  33125  cycpmconjv  33135  cycpmrn  33136  rndrhmcl  33265  fracf1  33274  xrge0slmod  33341  lsmsnorb2  33385  qusbas2  33399  1arithidomlem2  33529  zringfrac  33547  rlmdim  33622  rgmoddimOLD  33623  circtopn  33783  tpr2rico  33858  xrge0mulc1cn  33887  lmxrge0  33898  esumpfinvallem  34038  esumcocn  34044  hasheuni  34049  esumcvg  34050  rossros  34144  measinblem  34184  aean  34208  sxbrsigalem3  34237  dya2iocival  34238  dya2iocucvr  34249  sxbrsigalem1  34250  sxbrsigalem2  34251  sxbrsigalem5  34253  sxbrsiga  34255  fiunelcarsg  34281  eulerpartlem1  34332  eulerpartgbij  34337  fibp1  34366  coinfliplem  34443  coinflipprob  34444  ballotlemfval  34454  ballotth  34502  sgnneg  34505  plymulx  34525  circlemethhgt  34620  hgt750lem2  34629  bnj1400  34811  bnj66  34836  bnj882  34902  lfuhgr  35085  derang0  35137  subfacp1lem1  35147  subfacp1lem6  35153  kur14lem7  35180  cvmsss2  35242  cvmliftlem8  35260  cvmliftlem10  35262  satfv1lem  35330  msubfval  35492  quad3  35638  bcprod  35700  bccolsum  35701  faclim  35708  pprodcnveq  35847  dfon4  35857  fobigcup  35864  dfiota3  35887  dfrecs2  35914  dfrdg4  35915  dfint3  35916  rankeq1o  36135  refssfne  36324  ssoninhaus  36414  onint1  36415  bj-rababw  36847  bj-inrab3  36895  bj-imdiridlem  37151  dissneq  37307  dffinxpf  37351  finxpreclem4  37360  rabiun  37553  ptrest  37579  poimirlem3  37583  poimirlem4  37584  poimirlem13  37593  poimirlem16  37596  poimirlem22  37602  poimirlem26  37606  poimirlem27  37607  poimirlem30  37610  cnambfre  37628  ftc1anclem8  37660  fnopabco  37683  abrexdom  37690  cncfres  37725  scottexf  38128  scott0f  38129  inres2  38201  dfres4  38249  xrnres  38358  xrnres2  38359  dfcoss2  38369  dfcoss4  38371  1cossres  38385  dmcoss2  38410  1cosscnvxrn  38431  dfeqvrels2  38544  dfcoeleqvrels  38577  redundss3  38584  dffunsALTV5  38643  cdleme3d  40188  cdleme7a  40200  cdleme31sdnN  40344  cdlemk45  40904  420gcd8e4  41963  lcmeprodgcdi  41964  60lcm7e420  41967  420lcm8e840  41968  3lexlogpow5ineq1  42011  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1p1  42033  posbezout  42057  aks6d1c1p4  42068  aks6d1c3  42080  2ap1caineq  42102  sticksstones7  42109  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem4  42130  imaopab  42224  fmpocos  42229  dfqs2  42232  dfqs3  42233  decaddcom  42273  sumcubes  42301  sn-00idlem2  42375  reixi  42398  sum9cubes  42627  mapfzcons  42672  eldioph4b  42767  diophren  42769  pwssplit4  43046  pwfi2f1o  43053  frlmpwfi  43055  mendplusgfval  43142  mendmulrfval  43144  mendvscafval  43147  idomodle  43152  cytpval  43163  arearect  43176  onov0suclim  43236  omabs2  43294  tr3dom  43490  har2o  43508  alephiso2  43520  alephiso3  43521  relintab  43545  dfid7  43574  cnvrcl0  43587  dfrtrcl5  43591  dfrcl3  43637  dfrcl4  43638  comptiunov2i  43668  corcltrcl  43701  neicvgnvo  44077  inductionexd  44117  mnuprdlem2  44242  nznngen  44285  hashnzfz2  44290  lhe4.4ex1a  44298  dvradcnv2  44316  binomcxplemrat  44319  binomcxplemnotnn0  44325  refsum2cnlem1  44937  fiiuncl  44967  iccdifprioo  45434  lptre2pt  45561  limclner  45572  stoweidlem13  45934  stoweidlem32  45953  stoweidlem62  45983  wallispi2lem2  45993  stirlinglem14  46008  dirkertrigeqlem1  46019  dirkercncflem4  46027  fourierdlem42  46070  fourierdlem73  46100  fourierdlem81  46108  fourierdlem92  46119  fourierdlem103  46130  fourierdlem104  46131  fouriercnp  46147  fouriersw  46152  sge0tsms  46301  sge0iunmptlemfi  46334  ovolval5lem3  46575  cnfsmf  46661  rnfdmpr  47196  fvmptrabdm  47208  fundcmpsurinjlem1  47272  m11nprm  47475  opoeALTV  47557  nfermltl8rev  47616  sbgoldbo  47661  evengpop3  47672  clnbgrcl  47695  clnbgrnvtx0  47700  usgrexmpl2edg  47844  usgrexmpl2nb0  47846  usgrexmpl2nb3  47849  cznabel  47983  cznrng  47984  mpomptx2  48059  2sphere  48483  itscnhlinecirc02plem3  48518  inlinecirc02p  48521  icccldii  48598  dfnrm2  48611  dfnrm3  48612  amgmlemALT  48897