Theorem eqtr4i 2635

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  3eqtr2i  2638  3eqtr2ri  2639  3eqtr4i  2642  3eqtr4ri  2643  rabab  3196  cbvralcsf  3531  cbvrabcsf  3534  dfin5  3548  dfdif2  3549  uneqin  3837  unrab  3857  inrab  3858  inrab2  3859  difrab  3860  dfrab3ss  3864  rabun2  3865  difidALT  3903  rabxm  3915  elnelun  3918  difdifdir  4008  dfif3  4050  dfif5  4052  rabsnif  4202  tpidm  4237  ssunpr  4305  sstp  4307  dfint2  4412  iunrab  4503  uniiun  4509  intiin  4510  0iin  4514  mptv  4679  dfepfr  5023  epfrc  5024  xpundi  5094  xpundir  5095  csbcnv  5228  resiun2  5338  resopab  5366  opabresid  5374  dffr3  5417  dfse2  5418  cnvun  5457  imaundir  5465  imainrect  5494  cnvcnv2  5506  cnvcnvres  5516  dmtpop  5529  rnsnopg  5532  rnco2  5559  dmco  5560  co01  5567  unidmrn  5582  dfdm2  5584  predidm  5619  tz6.26  5628  dfmpt3  5927  mptun  5938  funcocnv2  6074  dffv2  6181  fnasrn  6317  fpr  6326  fmptap  6341  riotav  6516  dmoprab  6639  rnoprab2  6642  mpt2v  6648  mpt2mptx  6649  abrexex2g  7036  abrexex2  7040  1stval2  7076  2ndval2  7077  fo1st  7079  fo2nd  7080  xp2  7094  dfoprab4f  7117  offval22  7140  fmpt2co  7147  tposmpt2  7276  tposconst  7277  recsfval  7364  rdgsucmpt2  7413  frsucmpt2  7422  df2o3  7460  o1p1e2  7507  o2p2e4  7508  oarec  7529  omopthlem2  7623  ecqs  7698  qliftf  7722  erovlem  7730  mapsnf1o3  7792  ixp0x  7822  omf1o  7948  xpf1o  8007  mapunen  8014  enp1ilem  8079  pwfi  8144  marypha1lem  8222  marypha2lem4  8227  dfoi  8299  infeq5i  8416  oemapso  8462  cantnflem1  8469  rankelop  8620  leweon  8717  r0weon  8718  kmlem11  8865  infcda1  8898  ackbij1lem16  8940  cf0  8956  cfsmolem  8975  alephsuc3  9281  fpwwe  9347  canthp1lem1  9353  wuncval2  9448  prlem936  9748  m1p1sr  9792  m1m1sr  9793  dfcnqs  9842  ssxr  9986  mul02lem2  10092  addid1  10095  2p2e4  11021  3p2e5  11037  3p3e6  11038  4p2e6  11039  4p3e7  11040  4p4e8  11041  5p2e7  11042  5p3e8  11043  5p4e9  11044  5p5e10OLD  11045  6p2e8  11046  6p3e9  11047  6p4e10OLD  11048  7p2e9  11049  7p3e10OLD  11050  8p2e10OLD  11051  nnzrab  11282  nn0zrab  11283  dec0u  11396  dec0uOLD  11397  dec0h  11398  dec0hOLD  11399  decsuc  11411  decsucOLD  11412  decsucc  11426  decsuccOLD  11427  numma  11433  decma  11440  decmaOLD  11441  decmac  11442  decmacOLD  11443  decma2c  11444  decma2cOLD  11445  decadd  11446  decaddOLD  11447  decaddc  11448  decaddcOLD  11449  decmul1  11461  decmul1OLD  11462  decmul1c  11463  decmul1cOLD  11464  decmul2c  11465  decmul2cOLD  11466  5p5e10  11472  6p4e10  11474  7p3e10  11479  8p2e10  11486  5t5e25  11515  5t5e25OLD  11516  6t6e36  11522  6t6e36OLD  11523  8t6e48  11535  8t6e48OLD  11536  nn0uz  11598  nnuz  11599  xaddcom  11945  x2times  12001  ioomax  12119  iccmax  12120  ioopos  12121  ioorp  12122  prunioo  12172  fseq1p1m1  12283  fzo13pr  12419  fzo0to2pr  12420  fzo0to3tp  12421  om2uzrdg  12617  fzennn  12629  irec  12826  sq10e99m1  12911  sq10e99m1OLD  12914  facnn  12924  fac0  12925  faclbnd2  12940  faclbnd4lem1  12942  hashfun  13084  hashbclem  13093  hashf1lem1  13096  hashf1lem2  13097  fz1isolem  13102  swrdccatin1  13334  swrdccat3blem  13346  s1co  13430  s2eq2s1eq  13531  ofs2  13558  dfid5  13615  dfid6  13616  fsumrev2  14356  fsumparts  14379  fsumiun  14394  isumnn0nn  14413  harmonic  14430  0.999...OLD  14452  fprod2d  14550  bpoly2  14627  bpoly3  14628  bpoly4  14629  ege2le3  14659  cos1bnd  14756  efieq1re  14768  eirrlem  14771  qnnen  14781  cpnnen  14797  ruclem6  14803  3dvds  14890  3dvdsOLD  14891  pwp1fsum  14952  m1bits  15000  algrp1  15125  phiprmpw  15319  prmreclem4  15461  4sqlem11  15497  4sqlem19  15505  dec5dvds  15606  decsplit1  15624  decsplit1OLD  15628  5prm  15653  7prm  15655  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  ndxid  15716  strle1  15800  grpbasex  15819  grpplusgx  15820  quslem  16026  xpslem  16056  acsfn1  16145  acsfn2  16147  comfffval2  16184  xpchomfval  16642  xpccofval  16645  1stfval  16654  2ndfval  16657  oduleg  16955  ismgmid  17087  grpinvfvi  17286  gaorb  17563  cntri  17586  cntrsubgnsg  17596  cntrnsg  17597  oppglem  17603  oppgcntr  17618  gsumwrev  17619  symgbas  17623  symgga  17649  cayleylem1  17655  psgnunilem2  17738  efgval2  17960  efgredlemc  17981  efgcpbllema  17990  frgpnabllem1  18099  gsumzaddlem  18144  mgplem  18317  opprlem  18451  oppr0  18456  opprneg  18458  rlmscaf  19029  mplbas  19250  mpladd  19263  mplmul  19264  mplvsca2  19267  ressmplbas2  19276  ltbwe  19293  evlslem4  19329  psr1bas2  19381  ply1bas  19386  ply1assa  19390  mplplusg  19411  mplmulr  19412  psr1plusg  19413  psr1vsca  19414  psr1mulr  19415  ply1plusg  19416  ply1vsca  19417  ply1mulr  19418  ply1mpl0  19446  ply1mpl1  19448  coe1mul  19461  xrsds  19608  gsumfsum  19632  zringunit  19655  cnmsgngrp  19744  psgnfix2  19764  relt  19780  ocv0  19840  thlle  19860  thlleval  19861  dsmmval2  19899  frlmip  19936  matgsum  20062  smadiadetglem1  20296  indistpsx  20624  iuncld  20659  tgrest  20773  resstopn  20800  leordtval2  20826  xkouni  21212  ptclsg  21228  ptuncnv  21420  ptunhmeo  21421  alexsubALTlem4  21664  tsmsf1o  21758  ucnimalem  21894  ressxms  22140  uniretop  22376  cnfldtopn  22395  xrtgioo  22417  zcld  22424  icccmp  22436  xrge0gsumle  22444  xrge0tsms  22445  metnrmlem3  22472  fsum2cn  22482  cnmpt2pc  22535  oprpiece1res1  22558  oprpiece1res2  22559  evth  22566  evth2  22567  om1opn  22644  pi1xfrf  22661  pi1xfrcnv  22665  pi1cof  22667  clsocv  22857  cncmet  22927  cnflduss  22960  rrxprds  22985  ehlbase  23002  ismbl  23101  shftmbl  23113  ioorinv  23150  itg1addlem4  23272  itg2cnlem1  23334  iblitg  23341  itg0  23352  itgss3  23387  ditgneg  23427  limcdif  23446  limciun  23464  dvexp  23522  dvef  23547  dvcnvrelem2  23585  ftc1  23609  plyremlem  23863  aannenlem2  23888  taylply2  23926  dvradcnv  23979  pserdvlem2  23986  reefgim  24008  cospi  24028  sincos6thpi  24071  tanregt0  24089  dflog2  24111  logfac  24151  dvlog  24197  cxpexp  24214  cxpmul2  24235  cxpsqrt  24249  dvsqrt  24283  dvcnsqrt  24285  cxpcn2  24287  ang180lem2  24340  isosctrlem2  24349  1cubrlem  24368  1cubr  24369  quart1lem  24382  atancj  24437  atanlogaddlem  24440  atansopn  24459  leibpilem2  24468  log2cnv  24471  log2ublem3  24475  birthdaylem1  24478  birthdaylem2  24479  birthday  24481  dfarea  24487  lgamgulmlem5  24559  lgambdd  24563  wilthlem2  24595  ftalem3  24601  ftalem7  24605  basellem2  24608  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  ppi2  24696  ppi3  24697  ppiub  24729  chtub  24737  bclbnd  24805  bposlem8  24816  lgsdilem  24849  lgsdir2lem1  24850  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsquadlem2  24906  lgsquad2lem2  24910  2lgsoddprmlem3c  24937  rplogsum  25016  mulog2sumlem2  25024  pnt2  25102  istrkg2ld  25159  axsegconlem9  25605  ax5seglem7  25615  usgrares1  25939  cusgrares  26001  wwlknprop  26214  wwlknfi  26266  wlknwwlknvbij  26268  clwwlkvbij  26329  eupath2lem3  26506  ex-pw  26678  ex-xp  26685  ex-rn  26689  nvvop  26848  nvm  26880  cnims  26932  ip0i  27064  ip1ilem  27065  ipdirilem  27068  ipasslem10  27078  h2hva  27215  h2hsm  27216  h2hvs  27218  axhfvadd-zf  27223  axhvcom-zf  27224  axhvass-zf  27225  axhv0cl-zf  27226  axhvaddid-zf  27227  axhfvmul-zf  27228  axhvmulid-zf  27229  axhvmulass-zf  27230  axhvdistr1-zf  27231  axhvdistr2-zf  27232  axhvmul0-zf  27233  axhfi-zf  27234  axhis1-zf  27235  axhis2-zf  27236  axhis3-zf  27237  axhis4-zf  27238  axhcompl-zf  27239  normlem0  27350  normlem1  27351  normlem2  27352  normlem4  27354  normlem9  27359  bcseqi  27361  dfhnorm2  27363  norm3difi  27388  normpari  27395  normpar2i  27397  polid2i  27398  polidi  27399  hhba  27408  hhims  27413  hhims2  27414  hhsssh  27510  hhssims  27516  hhssims2  27517  shsval3i  27631  dfch2  27650  cmcm2i  27836  fh2  27862  qlaxr3i  27879  spansnji  27889  pjcji  27927  ho0val  27993  df0op2  27995  hosd1i  28065  hosd2i  28066  eigorthi  28080  hhlnoi  28143  hhnmoi  28144  hhbloi  28145  bra0  28193  nmop0  28229  nmfn0  28230  lnopeq0lem1  28248  lnopunilem1  28253  lnophmlem2  28260  nmopcoadji  28344  pjhmopidm  28426  cvmdi  28567  cdj3lem3  28681  cdj3lem3b  28683  abrexdomjm  28729  uniin1  28750  uniin2  28751  iundifdifd  28762  iundifdif  28763  mpt2mptxf  28860  df1stres  28864  df2ndres  28865  fcobijfs  28889  resf1o  28893  fpwrelmapffslem  28895  xrslt  29007  xrsclat  29011  gsumle  29110  xrge0tsmsd  29116  xrge0slmod  29175  fimaproj  29228  circtopn  29232  tpr2rico  29286  xrge0mulc1cn  29315  lmxrge0  29326  esumpfinvallem  29463  esumcocn  29469  hasheuni  29474  esumcvg  29475  rossros  29570  measinblem  29610  aean  29634  sxbrsigalem3  29661  dya2iocival  29662  dya2iocucvr  29673  sxbrsigalem1  29674  sxbrsigalem2  29675  sxbrsigalem5  29677  sxbrsiga  29679  fiunelcarsg  29705  eulerpartlem1  29756  eulerpartgbij  29761  fibp1  29790  coinfliplem  29867  coinflipprob  29868  ballotlemfval  29878  ballotth  29926  sgnneg  29929  plymulx  29951  bnj1400  30160  bnj66  30184  bnj882  30250  derang0  30405  subfacp1lem1  30415  subfacp1lem6  30421  kur14lem7  30448  cvmsss2  30510  cvmliftlem8  30528  cvmliftlem10  30530  msubfval  30675  quad3  30818  bcprod  30877  bccolsum  30878  faclim  30885  dftrpred2  30963  bdayfo  31074  pprodcnveq  31160  dfon4  31170  fobigcup  31177  dfiota3  31200  dfrecs2  31227  dfrdg4  31228  dfint3  31229  rankeq1o  31448  refssfne  31523  ssoninhaus  31617  onint1  31618  bj-rababwv  32061  bj-inrab3  32117  rnmptsn  32358  dissneq  32364  dffinxpf  32398  finxpreclem4  32407  rabiun  32552  ptrest  32578  poimirlem3  32582  poimirlem4  32583  poimirlem13  32592  poimirlem16  32595  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  poimirlem30  32609  cnambfre  32628  ftc1anclem8  32662  fnopabco  32687  abrexdom  32695  cncfres  32734  scottexf  33146  scott0f  33147  cdleme3d  34536  cdleme7a  34548  cdleme31sdnN  34693  cdlemk45  35253  mapfzcons  36297  eldioph4b  36393  diophren  36395  pwssplit4  36677  pwfi2f1o  36684  frlmpwfi  36686  mendplusgfval  36774  mendmulrfval  36776  mendvscafval  36779  idomodle  36793  cytpval  36806  arearect  36820  relintab  36908  dfid7  36938  cnvrcl0  36951  dfrtrcl5  36955  dfrcl3  36986  dfrcl4  36987  comptiunov2i  37017  corcltrcl  37050  neicvgnvo  37433  inductionexd  37473  nznngen  37537  hashnzfz2  37542  lhe4.4ex1a  37550  dvradcnv2  37568  binomcxplemrat  37571  binomcxplemnotnn0  37577  compne  37665  refsum2cnlem1  38219  fiiuncl  38259  rnmptc  38348  iccdifprioo  38589  lptre2pt  38707  limclner  38718  stoweidlem13  38906  stoweidlem32  38925  stoweidlem62  38955  wallispi2lem2  38965  stirlinglem14  38980  dirkertrigeqlem1  38991  dirkercncflem4  38999  fourierdlem42  39042  fourierdlem73  39072  fourierdlem81  39080  fourierdlem92  39091  fourierdlem103  39102  fourierdlem104  39103  fouriercnp  39119  fouriersw  39124  sge0tsms  39273  sge0iunmptlemfi  39306  ovolval5lem3  39544  cnfsmf  39627  m11nprm  40056  opoeALTV  40132  evengpop3  40214  rnfdmpr  40325  nbgrnvtx0  40563  rusgrprc  40790  wwlksnfi  41112  wlksnwwlknvbij  41114  clwwlksvbij  41229  konigsbergumgr  41420  konigsbergupgrOLD  41421  cznabel  41746  cznrng  41747  mpt2mptx2  41906  amgmlemALT  42358