Theorem eqtr3i 2764

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

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

Assertion

Ref	Expression
eqtr3i	⊢ 𝐵 = 𝐶

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2743	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2762	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  3eqtr3i  2770  3eqtr3ri  2771  rabrabiOLD  3458  unundi  4185  unundir  4186  inindi  4242  inindir  4243  dfin4  4283  difun1  4304  difabs  4308  notab  4319  dif0  4383  disjdifr  4478  difdifdir  4497  pwundif  4628  tpidm13  4760  intmin2  4979  iunxdif3  5099  univ  5461  iunxpconst  5760  rnresi  6094  rnresv  6222  cnvsn0  6231  resdmres  6253  coi2  6284  coires1  6285  dfdm2  6302  isarep2  6658  resasplit  6778  ssimaex  6993  fnreseql  7067  resfunexg  7234  mpompt  7546  caov31  7661  fvresex  7982  xpexgALT  8004  1st2val  8040  2nd2val  8041  cnvoprab  8083  fnsuppeq0  8215  ecopovtrn  8858  limensuci  9191  pwfilem  9353  r1sucg  9806  jech9.3  9851  rankbnd2  9906  djuin  9955  compss  10413  zorn2lem4  10536  iunfo  10576  cardf  10587  alephsuc3  10617  fpwwe2lem12  10679  rankcf  10814  halfnq  11013  addclprlem2  11054  mulgt0sr  11142  mul02lem2  11435  mul02  11436  addrid  11438  mvlladdi  11524  mvllmuli  12097  infrenegsup  12248  8th4div3  12483  nneo  12699  nummac  12775  numadd  12777  numaddc  12778  nummul1c  12779  decbin0  12870  rpsup  13902  resup  13903  om2uzrdg  13993  m1expcl2  14122  facnn  14310  fac0  14311  faclbnd4lem1  14328  4bc3eq4  14363  hasheq0  14398  f1oun2prg  14952  sqrt1  15306  sqrt4  15307  sqrt9  15308  rddif  15375  abs3lemi  15445  sumss2  15758  divcnvshft  15887  geo2sum2  15906  geomulcvg  15908  geoihalfsum  15914  risefall0lem  16058  bpoly2  16089  bpoly3  16090  sin0  16181  efival  16184  ef01bndlem  16216  cos2bnd  16220  sin4lt0  16227  flodddiv4  16448  2prm  16725  unbenlem  16941  dec5dvds  17097  modxai  17101  mod2xi  17102  mod2xnegi  17104  gcdi  17106  numexp2x  17112  decsplit  17116  setsid  17241  mreexexlem3d  17690  oppchom  17760  2oppchomf  17770  isoval  17812  estrres  18194  oppchofcl  18316  oyoncl  18326  mvdco  19477  m1expaddsub  19530  psgn0fv0  19543  oppglsm  19674  dprd2da  20076  ring1  20323  opprsubg  20368  lsppratlem1  21166  pzriprnglem7  21515  zzngim  21588  cnmsgnsubg  21612  psgninv  21617  zrhpsgnmhm  21619  ply1basfvi  22257  coe1tm  22291  ply1coe  22317  comppfsc  23555  kgeni  23560  xkoinjcn  23710  ufprim  23932  metreslem  24387  retopbas  24796  cnfldms  24811  qdensere2  24832  xrsmopn  24847  metdscn2  24892  pcoass  25070  recvs  25192  recvsOLD  25193  zclmncvs  25195  iscmet3lem3  25337  cncms  25402  cnfldcusp  25404  resscdrg  25405  rrxprds  25436  ovoliunnul  25555  uniioombllem4  25634  vitalilem5  25660  mbfres  25692  ismbf3d  25702  i1fima  25726  i1fd  25729  itg2cnlem1  25810  itgss3  25864  ellimc2  25926  limccnp2  25941  cpnres  25987  lhop  26069  plyeq0  26264  plypf1  26265  sinhalfpilem  26519  sincos6thpi  26572  sincos3rdpi  26573  pige3ALT  26576  dfrelog  26621  logi  26643  logimul  26670  logneg2  26671  dvlog  26707  cxpsqrt  26759  ang180lem2  26867  ang180lem3  26868  ang180lem4  26869  quart1  26913  asin1  26951  atan0  26965  atanlogsublem  26972  atan1  26985  log2tlbnd  27002  log2ublem2  27004  log2ub  27006  basellem8  27145  cht2  27229  ppiub  27262  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem3  27385  lgseisenlem1  27433  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  2lgsoddprmlem2  27467  chebbnd1  27530  negsbdaylem  28102  om2noseqrdg  28324  zseo  28420  istrkg3ld  28483  tgcgr4  28553  motplusg  28564  ax5seglem7  28964  ex-un  30452  ex-sqrt  30482  ipdirilem  30857  ipasslem10  30867  hisubcomi  31132  normlem0  31137  norm3difi  31175  norm3lem  31177  polid2i  31185  chdmj1i  31509  chjjdiri  31552  spansn0  31569  pjoml4i  31615  cmbr3i  31628  qlaxr3i  31664  honpcani  31853  honpncani  31855  lnopunilem1  32038  lnophmlem2  32045  lnfn0i  32070  pjbdlni  32177  pjclem1  32223  pjclem3  32225  pjci  32228  atomli  32410  atabs2i  32430  mddmdin0i  32459  imadifxp  32620  fnresin  32642  ofpreima2  32682  df1stres  32718  df2ndres  32719  cnvoprabOLD  32737  nn0disj01  32824  dfdec100  32836  decdiv10  32862  dpmul100  32863  dpmul1000  32865  dpexpp1  32874  dpadd2  32876  dpadd  32877  dpmul  32879  dpmul4  32880  threehalves  32881  xrge0base  32998  xrge00  32999  xrge0mulgnn0  33002  cyc2fv1  33123  cyc3conja  33159  elrgspnlem4  33234  xrge0slmod  33355  opprqusplusg  33496  opprqusmulr  33498  lmatfvlem  33775  xrge0iifcnv  33893  lmxrge0  33912  cnrrext  33972  qqtopn  33973  esumrnmpt2  34048  esumpfinvallem  34054  unelldsys  34138  ldgenpisyslem1  34143  measunl  34196  mbfmcst  34240  difelcarsg  34291  carsggect  34299  sibfof  34321  eulerpartlemmf  34356  fib2  34383  fib3  34384  fib4  34385  fib5  34386  fib6  34387  0rrv  34432  coinfliprv  34463  ballotlem2  34469  prodfzo03  34596  chtvalz  34622  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  kur14lem6  35195  kur14lem7  35196  cvmlift2lem12  35298  problem5  35653  quad3  35654  divcnvlin  35712  in-ax8  36206  bj-2upln1upl  37006  bj-rest0  37075  relowlssretop  37345  relowlpssretop  37346  1oequni2o  37350  curunc  37588  ptrest  37605  poimirlem16  37622  poimirlem30  37636  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  itg2addnclem2  37658  ftc1anclem5  37683  ftc1anclem6  37684  sdc  37730  heiborlem3  37799  xrnresex  38387  dvh4dimN  41429  12gcd5e1  41984  60gcd6e6  41985  60gcd7e1  41986  420gcd8e4  41987  lcmeprodgcdi  41988  lcmineqlem23  42032  sq3deccom12  42303  asin1half  42365  acos1half  42366  redvmptabs  42368  sn-it1ei  42442  sn-0tie0  42445  sn-inelr  42473  dnnumch1  43032  aomclem6  43047  areaquad  43204  naddov4  43372  unitadd  44184  seff  44304  sblpnf  44305  hashnzfz  44315  lhe4.4ex1a  44324  xrtgcntopre  45428  iccdifioo  45467  itgsin0pilem1  45905  stoweidlem13  45968  stoweidlem26  45981  fourierdlem62  46123  fourierdlem102  46163  fourierdlem114  46175  fourierswlem  46185  fouriersw  46186  sge0tsms  46335  meaiuninc  46436  tworepnotupword  46839  fmtno4prmfac  47496  41prothprm  47543  dfclnbgr4  47748  2zrngasgrp  48089  2zrngmsgrp  48096  mvlraddi  49001  mvlrmuli  49007  i2linesi  49008