Theorem eqtr3i 2794

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  3eqtr3i  2800  3eqtr3ri  2801  unundi  4137  unundir  4138  inindi  4195  inindir  4196  dfin4  4239  difun1  4260  difabs  4264  notab  4275  dif0  4341  difdifdir  4457  pwundif  4592  tpidm13  4727  intmin2  4944  iunxdif3  5065  univ  5433  iunxpconst  5735  resdmdfsn  6032  rnresi  6078  rnresv  6201  imadifssran  6203  cnvsn0  6212  resdmres  6234  coi2  6266  coires1  6267  dfdm2  6283  isarep2  6626  resasplit  6749  ssimaex  6967  fnreseql  7044  resfunexg  7214  mpompt  7525  caov31  7640  fvresex  7956  xpexgALT  7977  1st2val  8013  2nd2val  8014  cnvoprab  8056  fnsuppeq0  8187  ecopovtrn  8817  limensuci  9140  pwfilem  9276  r1sucg  9740  jech9.3  9785  rankbnd2  9840  djuin  9903  compss  10359  zorn2lem4  10482  iunfo  10522  cardf  10533  alephsuc3  10564  fpwwe2lem12  10626  rankcf  10761  halfnq  10960  addclprlem2  11001  mulgt0sr  11089  mul02lem2  11386  mul02  11387  addrid  11389  mvlladdi  11475  mvllmuli  12047  infrenegsup  12197  8th4div3  12463  halfpm6th  12465  nneo  12679  nummac  12760  numadd  12762  numaddc  12763  nummul1c  12764  decbin0  12857  rpsup  13898  resup  13899  om2uzrdg  13991  m1expcl2  14120  facnn  14310  fac0  14311  faclbnd4lem1  14328  4bc3eq4  14363  hasheq0  14398  f1oun2prg  14953  sqrt1  15321  sqrt4  15322  sqrt9  15323  rddif  15391  abs3lemi  15461  sumss2  15776  divcnvshft  15908  geo2sum2  15927  geomulcvg  15929  geoihalfsum  15935  risefall0lem  16079  bpoly2  16110  bpoly3  16111  sin0  16204  efival  16207  ef01bndlem  16239  cos2bnd  16243  sin4lt0  16250  flodddiv4  16472  2prm  16749  unbenlem  16967  dec5dvds  17123  modxai  17127  mod2xi  17128  mod2xnegi  17130  gcdi  17132  numexp2x  17137  decsplit  17141  setsid  17266  xrge0base  17660  mreexexlem3d  17701  oppchom  17770  2oppchomf  17779  isoval  17821  estrres  18194  oppchofcl  18315  oyoncl  18325  mvdco  19514  m1expaddsub  19567  psgn0fv0  19580  oppglsm  19711  dprd2da  20113  ring1  20392  opprsubg  20433  lsppratlem1  21248  pzriprnglem7  21605  zzngim  21670  cnmsgnsubg  21695  psgninv  21700  zrhpsgnmhm  21702  ply1basfvi  22368  coe1tm  22402  ply1coe  22426  comppfsc  23657  kgeni  23662  xkoinjcn  23812  ufprim  24034  metreslem  24487  retopbas  24885  cnfldms  24900  qdensere2  24922  xrsmopn  24938  metdscn2  24983  pcoass  25151  recvs  25273  zclmncvs  25275  iscmet3lem3  25417  cncms  25482  cnfldcusp  25484  resscdrg  25485  rrxprds  25516  ovoliunnul  25634  uniioombllem4  25713  vitalilem5  25739  mbfres  25771  ismbf3d  25781  i1fima  25805  i1fd  25808  itg2cnlem1  25888  itgss3  25942  ellimc2  26004  limccnp2  26019  cpnres  26064  lhop  26143  plyeq0  26336  plypf1  26337  sinhalfpilem  26593  sincos6thpi  26646  sincos3rdpi  26647  pige3ALT  26650  dfrelog  26695  logi  26717  logimul  26744  logneg2  26745  dvlog  26781  cxpsqrt  26833  ang180lem2  26940  ang180lem3  26941  ang180lem4  26942  quart1  26986  asin1  27024  atan0  27038  atanlogsublem  27045  atan1  27058  log2tlbnd  27075  log2ublem2  27077  log2ub  27079  basellem8  27217  cht2  27301  ppiub  27333  bposlem6  27418  bposlem8  27420  bposlem9  27421  lgsdir2lem3  27456  lgseisenlem1  27504  lgseisenlem2  27505  lgsquadlem1  27509  lgsquadlem2  27510  2lgsoddprmlem2  27538  chebbnd1  27601  negbdaylem  28214  om2noseqrdg  28462  zseo  28580  bdaypw2n0bndlem  28621  istrkg3ld  28695  tgcgr4  28765  motplusg  28776  ax5seglem7  29225  ex-un  30715  ex-sqrt  30745  ipdirilem  31121  ipasslem10  31131  hisubcomi  31396  normlem0  31401  norm3difi  31439  norm3lem  31441  polid2i  31449  chdmj1i  31773  chjjdiri  31816  spansn0  31833  pjoml4i  31879  cmbr3i  31892  qlaxr3i  31928  honpcani  32117  honpncani  32119  lnopunilem1  32302  lnophmlem2  32309  lnfn0i  32334  pjbdlni  32441  pjclem1  32487  pjclem3  32489  pjci  32492  atomli  32674  atabs2i  32694  mddmdin0i  32723  imadifxp  32886  fnresin  32909  ofpreima2  32951  df1stres  32989  df2ndres  32990  nn0disj01  33103  dfdec100  33114  decdiv10  33155  dpmul100  33156  dpmul1000  33158  dpexpp1  33167  dpadd2  33169  dpadd  33170  dpmul  33172  dpmul4  33173  threehalves  33174  xrge00  33274  xrge0mulgnn0  33275  cyc2fv1  33381  cyc3conja  33417  elrgspnlem4  33505  xrge0slmod  33610  opprqusplusg  33715  opprqusmulr  33717  selvply1rhmlemb  33853  extvfvcl  33870  2sqr3nconstr  34115  cos9thpiminplylem1  34116  cos9thpiminplylem5  34120  cos9thpinconstrlem2  34124  lmatfvlem  34149  xrge0iifcnv  34267  lmxrge0  34286  cnrrext  34344  qqtopn  34345  esumrnmpt2  34402  esumpfinvallem  34408  unelldsys  34492  ldgenpisyslem1  34497  measunl  34550  mbfmcst  34593  difelcarsg  34644  carsggect  34652  sibfof  34674  eulerpartlemmf  34709  fib2  34736  fib3  34737  fib4  34738  fib5  34739  fib6  34740  0rrv  34785  coinfliprv  34817  ballotlem2  34823  prodfzo03  34934  chtvalz  34960  hgt750lemd  34979  hgt750lem  34982  hgt750lem2  34983  1enumen  35427  kur14lem6  35601  kur14lem7  35602  cvmlift2lem12  35704  problem5  36059  quad3  36060  divcnvlin  36123  in-ax8  36624  bj-2upln1upl  37547  bj-rest0  37622  relowlssretop  37896  relowlpssretop  37897  1oequni2o  37901  curunc  38140  ptrest  38157  poimirlem16  38174  poimirlem30  38188  mblfinlem2  38196  ovoliunnfl  38200  voliunnfl  38202  itg2addnclem2  38210  ftc1anclem5  38235  ftc1anclem6  38236  sdc  38282  heiborlem3  38351  xrnresex  38967  dmxrncnvepres  38970  dvh4dimN  42110  12gcd5e1  42659  60gcd6e6  42660  60gcd7e1  42661  420gcd8e4  42662  lcmeprodgcdi  42663  lcmineqlem23  42707  25or6to4  42862  sq3deccom12  42940  asin1half  43007  acos1half  43008  redvmptabs  43010  readvrec  43012  sn-it1ei  43087  sn-0tie0  43114  dnnumch1  43662  aomclem6  43677  areaquad  43834  naddov4  44001  unitadd  44812  seff  44910  sblpnf  44911  hashnzfz  44921  lhe4.4ex1a  44930  xrtgcntopre  46083  iccdifioo  46122  itgsin0pilem1  46555  stoweidlem13  46618  stoweidlem26  46631  fourierdlem62  46773  fourierdlem102  46813  fourierdlem114  46825  fourierswlem  46835  fouriersw  46836  sge0tsms  46985  meaiuninc  47086  cos5t  47504  fmtno4prmfac  48212  41prothprm  48259  ppivalnn4  48267  dfclnbgr4  48477  2zrngasgrp  48899  2zrngmsgrp  48906  tposres3  49543  eloppf  49795  setc1onsubc  50264  mvlraddi  50433  mvlrmuli  50439  i2linesi  50440