Theorem eqtr4i 2822

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 2804	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2819	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788

This theorem is referenced by:  3eqtr2i  2825  3eqtr2ri  2826  3eqtr4i  2829  3eqtr4ri  2830  rabab  3466  cbvralcsf  3849  cbvrabcsf  3852  dfin5  3867  dfdif2  3868  uneqin  4175  unrab  4194  inrab  4195  inrab2  4196  difrab  4197  dfrab3ss  4201  rabun2  4202  difidALT  4251  rabxm  4260  elnelun  4263  difdifdir  4351  dfif3  4395  dfif5  4397  rabsnif  4566  tpidm  4601  ssunpr  4672  sstp  4674  opidg  4729  dfint2  4784  iunrab  4875  uniiun  4881  intiin  4882  0iin  4886  mptv  5062  dfepfr  5428  epfrc  5429  xpundi  5506  xpundir  5507  csbcnv  5640  resiun2  5755  resopab  5783  opabresid  5797  dffr3  5838  dfse2  5839  cnvun  5877  imaundir  5885  imainrect  5914  cnvcnv2  5926  cnvcnvres  5937  dmtpop  5950  rnsnopg  5953  rnco2  5981  dmco  5982  co01  5989  unidmrn  6005  dfdm2  6007  predidm  6045  tz6.26  6054  dfmpt3  6350  mptun  6362  funcocnv2  6507  dffv2  6623  fnasrn  6770  fpr  6779  fmptap  6795  rnmptc  6836  riotav  6982  dmoprab  7111  rnoprab2  7114  mpov  7120  mpomptx  7121  abrexex2g  7521  1stval2  7562  2ndval2  7563  fo1st  7565  fo2nd  7566  xp2  7582  dfoprab4f  7610  offval22  7639  fmpoco  7646  tposmpo  7780  tposconst  7781  recsfval  7869  rdgsucmpt2  7918  frsucmpt2  7927  df2o3  7968  o1p1e2  8016  o2p2e4  8017  oarec  8038  omopthlem2  8133  ecqs  8211  qliftf  8235  erovlem  8243  mapsnf1o3  8308  ixp0x  8338  omf1o  8467  xpf1o  8526  mapunen  8533  enp1ilem  8598  pwfi  8665  marypha1lem  8743  marypha2lem4  8748  dfoi  8821  infeq5i  8945  oemapso  8991  cantnflem1  8998  rankelop  9149  leweon  9283  r0weon  9284  kmlem11  9432  dju1dif  9444  ackbij1lem16  9503  cf0  9519  cfsmolem  9538  alephsuc3  9848  fpwwe  9914  canthp1lem1  9920  wuncval2  10015  prlem936  10315  m1p1sr  10360  m1m1sr  10361  dfcnqs  10410  ssxr  10557  mul02lem2  10664  addid1  10667  2p2e4  11620  3p2e5  11636  3p3e6  11637  4p2e6  11638  4p3e7  11639  4p4e8  11640  5p2e7  11641  5p3e8  11642  5p4e9  11643  6p2e8  11644  6p3e9  11645  7p2e9  11646  nnzrab  11859  nn0zrab  11860  dec0u  11968  dec0h  11969  decsuc  11978  decsucc  11988  numma  11991  decma  11998  decmac  11999  decma2c  12000  decadd  12001  decaddc  12002  decmul1OLD  12012  decmul1c  12013  decmul2c  12014  5p5e10  12019  6p4e10  12020  7p3e10  12023  8p2e10  12028  5t5e25  12051  6t6e36  12056  8t6e48  12067  nn0uz  12129  nnuz  12130  xaddcom  12483  x2times  12542  ioomax  12661  iccmax  12662  ioopos  12663  ioorp  12664  prunioo  12717  fseq1p1m1  12831  fzo13pr  12971  fzo0to2pr  12972  fzo0to3tp  12973  om2uzrdg  13174  fzennn  13186  irec  13414  sq10e99m1  13475  facnn  13485  fac0  13486  faclbnd2  13501  faclbnd4lem1  13503  hashfun  13646  hashbclem  13658  hashf1lem1  13661  hashf1lem2  13662  fz1isolem  13667  swrdccatin1  13923  swrdccat3blem  13937  s1co  14031  s2eq2s1eq  14134  s3eqs2s1eq  14136  ofs2  14165  dfid5  14220  dfid6  14221  fsumrev2  14970  fsumparts  14994  fsumiun  15009  isumnn0nn  15030  harmonic  15047  fprod2d  15168  bpoly2  15244  bpoly3  15245  bpoly4  15246  ege2le3  15276  cos1bnd  15373  efieq1re  15385  eirrlem  15390  qnnen  15399  cpnnen  15415  ruclem6  15421  3dvds  15513  pwp1fsum  15575  m1bits  15622  algrp1  15747  phiprmpw  15942  prmreclem4  16084  4sqlem11  16120  4sqlem19  16128  dec5dvds  16229  decsplit1  16247  5prm  16271  7prm  16273  1259lem2  16294  1259lem3  16295  1259lem4  16296  1259lem5  16297  1259prm  16298  2503lem1  16299  2503lem2  16300  2503lem3  16301  2503prm  16302  4001lem1  16303  4001lem2  16304  4001lem3  16305  4001lem4  16306  4001prm  16307  strle1  16421  grpbasex  16442  grpplusgx  16443  quslem  16645  xpsrnbas  16673  acsfn1  16761  acsfn2  16763  comfffval2  16800  xpchomfval  17258  xpccofval  17261  1stfval  17270  2ndfval  17273  oduleg  17571  ismgmid  17703  grpinvfvi  17903  gaorb  18178  cntri  18202  cntrsubgnsg  18212  cntrnsg  18213  oppglem  18219  oppgcntr  18234  gsumwrev  18235  symgbas  18239  symgga  18265  cayleylem1  18271  psgnunilem2  18354  efgval2  18577  efgredlemc  18598  efgcpbllema  18607  frgpnabllem1  18716  gsumzaddlem  18761  mgplem  18934  opprlem  19068  oppr0  19073  opprneg  19075  rmodislmod  19392  rlmscaf  19670  mplbas  19897  mpladd  19910  mplmul  19911  mplvsca2  19914  ressmplbas2  19923  ltbwe  19940  evlslem4  19975  psr1bas2  20041  ply1bas  20046  ply1assa  20050  mplplusg  20071  mplmulr  20072  psr1plusg  20073  psr1vsca  20074  psr1mulr  20075  ply1plusg  20076  ply1vsca  20077  ply1mulr  20078  ply1mpl0  20106  ply1mpl1  20108  coe1mul  20121  xrsds  20270  gsumfsum  20294  zringunit  20317  cnmsgngrp  20405  psgnfix2  20425  relt  20441  ocv0  20503  thlle  20523  thlleval  20524  dsmmval2  20562  frlmip  20604  matgsum  20730  smadiadetglem1  20964  indistpsx  21302  iuncld  21337  tgrest  21451  resstopn  21478  leordtval2  21504  xkouni  21891  ptclsg  21907  ptuncnv  22099  ptunhmeo  22100  alexsubALTlem4  22342  tsmsf1o  22436  ucnimalem  22572  ressxms  22818  uniretop  23054  cnfldtopn  23073  xrtgioo  23097  zcld  23104  icccmp  23116  xrge0gsumle  23124  xrge0tsms  23125  metnrmlem3  23152  fsum2cn  23162  cnmpopc  23215  oprpiece1res1  23238  oprpiece1res2  23239  evth  23246  evth2  23247  om1opn  23323  pi1xfrf  23340  pi1xfrcnv  23344  pi1cof  23346  clsocv  23536  cncmet  23608  cnflduss  23642  rrxprds  23675  ehlbase  23701  ismbl  23810  shftmbl  23822  ioorinv  23860  itg1addlem4  23983  itg2cnlem1  24045  itg0  24063  itgss3  24098  ditgneg  24138  limcdif  24157  limciun  24175  dvexp  24233  dvef  24260  dvcnvrelem2  24298  ftc1  24322  plyremlem  24576  aannenlem2  24601  taylply2  24639  dvradcnv  24692  pserdvlem2  24699  reefgim  24721  cospi  24741  sincos6thpi  24784  tanregt0  24804  dflog2  24825  logfac  24865  dvlog  24915  cxpexp  24932  cxpmul2  24953  cxpsqrt  24967  dvsqrt  25004  dvcnsqrt  25006  cxpcn2  25008  isosctrlem2  25078  1cubrlem  25100  1cubr  25101  quart1lem  25114  atancj  25169  atanlogaddlem  25172  atansopn  25191  leibpilem2  25201  log2cnv  25204  log2ublem3  25208  birthdaylem1  25211  birthdaylem2  25212  birthday  25214  dfarea  25220  lgamgulmlem5  25292  lgambdd  25296  wilthlem2  25328  ftalem3  25334  ftalem7  25338  basellem2  25341  ppiprm  25410  ppinprm  25411  chtprm  25412  chtnprm  25413  ppi2  25429  ppi3  25430  ppiub  25462  chtub  25470  bclbnd  25538  bposlem8  25549  lgsdilem  25582  lgsdir2lem2  25584  lgsquadlem2  25639  lgsquad2lem2  25643  2lgsoddprmlem3c  25670  rplogsum  25785  mulog2sumlem2  25793  pnt2  25871  istrkg2ld  25928  axsegconlem9  26394  ax5seglem7  26404  iedgedg  26518  uspgrf1oedg  26641  nbgrcl  26800  nbgrnvtx0  26804  rusgrprc  27055  wlkiswwlks2lem4  27337  wlkiswwlks2lem5  27338  wwlksnfiOLD  27372  clwwlkvbij  27579  konigsbergumgr  27720  ex-pw  27900  ex-xp  27907  ex-rn  27911  nvvop  28077  nvm  28109  cnims  28161  ip0i  28293  ip1ilem  28294  ipdirilem  28297  ipasslem10  28307  h2hva  28442  h2hsm  28443  h2hvs  28445  axhfvadd-zf  28450  axhvcom-zf  28451  axhvass-zf  28452  axhv0cl-zf  28453  axhvaddid-zf  28454  axhfvmul-zf  28455  axhvmulid-zf  28456  axhvmulass-zf  28457  axhvdistr1-zf  28458  axhvdistr2-zf  28459  axhvmul0-zf  28460  axhfi-zf  28461  axhis1-zf  28462  axhis2-zf  28463  axhis3-zf  28464  axhis4-zf  28465  axhcompl-zf  28466  normlem0  28577  normlem1  28578  normlem2  28579  normlem4  28581  normlem9  28586  bcseqi  28588  dfhnorm2  28590  norm3difi  28615  normpari  28622  normpar2i  28624  polid2i  28625  polidi  28626  hhba  28635  hhims  28640  hhims2  28641  hhsssh  28737  hhssims  28742  hhssims2  28743  shsval3i  28856  dfch2  28875  cmcm2i  29061  fh2  29087  qlaxr3i  29104  spansnji  29114  pjcji  29152  ho0val  29218  df0op2  29220  hosd1i  29290  hosd2i  29291  eigorthi  29305  hhlnoi  29368  hhnmoi  29369  hhbloi  29370  bra0  29418  nmop0  29454  nmfn0  29455  lnopeq0lem1  29473  lnopunilem1  29478  lnophmlem2  29485  nmopcoadji  29569  pjhmopidm  29651  cvmdi  29792  cdj3lem3  29906  cdj3lem3b  29908  abrexdomjm  29959  uniin1  29992  uniin2  29993  iundifdifd  30003  iundifdif  30004  mpomptxf  30115  df1stres  30127  df2ndres  30128  fcobijfs  30147  resf1o  30154  fpwrelmapffslem  30156  dpval3  30254  dp3mul10  30258  dpadd2  30270  dpmul4  30274  xrslt  30337  xrsclat  30341  cycpmconjv  30421  cycpmrn  30422  gsumle  30494  xrge0tsmsd  30503  xrge0slmod  30571  rgmoddim  30612  fimaproj  30714  circtopn  30718  tpr2rico  30772  xrge0mulc1cn  30801  lmxrge0  30812  esumpfinvallem  30950  esumcocn  30956  hasheuni  30961  esumcvg  30962  rossros  31056  measinblem  31096  aean  31120  sxbrsigalem3  31147  dya2iocival  31148  dya2iocucvr  31159  sxbrsigalem1  31160  sxbrsigalem2  31161  sxbrsigalem5  31163  sxbrsiga  31165  fiunelcarsg  31191  eulerpartlem1  31242  eulerpartgbij  31247  fibp1  31276  coinfliplem  31353  coinflipprob  31354  ballotlemfval  31364  ballotth  31412  sgnneg  31415  plymulx  31435  circlemethhgt  31531  hgt750lem2  31540  bnj1400  31724  bnj66  31748  bnj882  31814  lfuhgr  31976  derang0  32025  subfacp1lem1  32035  subfacp1lem6  32041  kur14lem7  32068  cvmsss2  32130  cvmliftlem8  32148  cvmliftlem10  32150  satfv1lem  32218  msubfval  32380  quad3  32522  bcprod  32579  bccolsum  32580  faclim  32587  dftrpred2  32668  bdayfo  32792  pprodcnveq  32954  dfon4  32964  fobigcup  32971  dfiota3  32994  dfrecs2  33021  dfrdg4  33022  dfint3  33023  rankeq1o  33242  refssfne  33316  ssoninhaus  33406  onint1  33407  bj-rababw  33773  bj-inrab3  33822  dissneq  34172  dffinxpf  34216  finxpreclem4  34225  wl-dfrabsb  34411  rabiun  34415  ptrest  34441  poimirlem3  34445  poimirlem4  34446  poimirlem13  34455  poimirlem16  34458  poimirlem22  34464  poimirlem26  34468  poimirlem27  34469  poimirlem30  34472  cnambfre  34490  ftc1anclem8  34524  fnopabco  34549  abrexdom  34556  cncfres  34594  scottexf  34997  scott0f  34998  inres2  35057  dfres4  35101  xrnres  35200  xrnres2  35201  dfcoss2  35211  dfcoss4  35213  1cossres  35224  dmcoss2  35244  1cosscnvxrn  35265  dfeqvrels2  35373  dfcoeleqvrels  35406  redundss3  35413  dffunsALTV5  35470  cdleme3d  36917  cdleme7a  36929  cdleme31sdnN  37073  cdlemk45  37633  imaopab  38668  dfqs2  38671  dfqs3  38672  decaddcom  38711  nn0expgcd  38725  mapfzcons  38817  eldioph4b  38912  diophren  38914  pwssplit4  39193  pwfi2f1o  39200  frlmpwfi  39202  mendplusgfval  39289  mendmulrfval  39291  mendvscafval  39294  idomodle  39300  cytpval  39313  arearect  39326  tr3dom  39398  alephiso2  39421  alephiso3  39422  relintab  39447  dfid7  39476  cnvrcl0  39489  dfrtrcl5  39493  dfrcl3  39524  dfrcl4  39525  comptiunov2i  39555  corcltrcl  39588  neicvgnvo  39969  inductionexd  40009  mnuprdlem2  40125  nznngen  40205  hashnzfz2  40210  lhe4.4ex1a  40218  dvradcnv2  40236  binomcxplemrat  40239  binomcxplemnotnn0  40245  refsum2cnlem1  40852  fiiuncl  40885  iccdifprioo  41353  lptre2pt  41482  limclner  41493  stoweidlem13  41860  stoweidlem32  41879  stoweidlem62  41909  wallispi2lem2  41919  stirlinglem14  41934  dirkertrigeqlem1  41945  dirkercncflem4  41953  fourierdlem42  41996  fourierdlem73  42026  fourierdlem81  42034  fourierdlem92  42045  fourierdlem103  42056  fourierdlem104  42057  fouriercnp  42073  fouriersw  42078  sge0tsms  42224  sge0iunmptlemfi  42257  ovolval5lem3  42498  cnfsmf  42579  rnfdmpr  43016  fvmptrabdm  43028  m11nprm  43268  opoeALTV  43350  nfermltl8rev  43409  sbgoldbo  43454  evengpop3  43465  cznabel  43723  cznrng  43724  mpomptx2  43881  2sphere  44237  itscnhlinecirc02plem3  44272  inlinecirc02p  44275  amgmlemALT  44404