MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr4i Structured version   Visualization version   GIF version

Theorem eqtr4i 2847
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
StepHypRef Expression
1 eqtr4i.1 . 2 𝐴 = 𝐵
2 eqtr4i.2 . . 3 𝐶 = 𝐵
32eqcomi 2830 . 2 𝐵 = 𝐶
41, 3eqtri 2844 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  3eqtr2i  2850  3eqtr2ri  2851  3eqtr4i  2854  3eqtr4ri  2855  rabab  3524  cbvralcsf  3924  cbvrabcsf  3927  dfin5  3943  dfdif2  3944  uneqin  4254  unrab  4273  inrab  4274  inrab2  4275  difrab  4276  dfrab3ss  4280  rabun2  4281  difidALT  4330  rabxm  4339  elnelun  4342  difdifdir  4435  dfif3  4479  dfif5  4481  rabsnif  4653  tpidm  4688  ssunpr  4759  sstp  4761  opidg  4816  dfint2  4871  iunrab  4968  uniiun  4974  intiin  4975  0iin  4979  mptv  5163  dfepfr  5534  epfrc  5535  xpundi  5614  xpundir  5615  csbcnv  5748  resiun2  5868  resopab  5896  mptresid  5912  opabresidOLD  5913  dffr3  5956  dfse2  5957  cnvun  5995  imaundir  6003  imainrect  6032  cnvcnv2  6044  cnvrescnv  6046  cnvcnvres  6056  dmtpop  6069  rnsnopg  6072  rnco2  6100  dmco  6101  co01  6108  unidmrn  6124  dfdm2  6126  predidm  6164  tz6.26  6173  dfmpt3  6476  mptun  6488  funcocnv2  6633  dffv2  6750  fnasrn  6900  fpr  6909  fmptap  6925  rnmptc  6962  riotav  7108  dmoprab  7244  rnoprab2  7247  mpov  7253  mpomptx  7254  abrexex2g  7656  1stval2  7697  2ndval2  7698  fo1st  7700  fo2nd  7701  xp2  7717  dfoprab4f  7745  offval22  7774  fmpoco  7781  fimaproj  7820  tposmpo  7920  tposconst  7921  recsfval  8008  rdgsucmpt2  8057  frsucmpt2w  8066  frsucmpt2  8067  df2o3  8108  o1p1e2  8156  o2p2e4  8157  oarec  8178  omopthlem2  8273  ecqs  8351  qliftf  8375  erovlem  8383  mapsnf1o3  8448  ixp0x  8479  omf1o  8609  xpf1o  8668  mapunen  8675  enp1ilem  8741  pwfi  8808  marypha1lem  8886  marypha2lem4  8891  dfoi  8964  infeq5i  9088  oemapso  9134  cantnflem1  9141  rankelop  9292  leweon  9426  r0weon  9427  kmlem11  9575  dju1dif  9587  ackbij1lem16  9646  cf0  9662  cfsmolem  9681  alephsuc3  9991  fpwwe  10057  canthp1lem1  10063  wuncval2  10158  prlem936  10458  m1p1sr  10503  m1m1sr  10504  dfcnqs  10553  ssxr  10699  mul02lem2  10806  addid1  10809  2p2e4  11761  3p2e5  11777  3p3e6  11778  4p2e6  11779  4p3e7  11780  4p4e8  11781  5p2e7  11782  5p3e8  11783  5p4e9  11784  6p2e8  11785  6p3e9  11786  7p2e9  11787  nnzrab  11999  nn0zrab  12000  dec0u  12108  dec0h  12109  decsuc  12118  decsucc  12128  numma  12131  decma  12138  decmac  12139  decma2c  12140  decadd  12141  decaddc  12142  decmul1c  12152  decmul2c  12153  5p5e10  12158  6p4e10  12159  7p3e10  12162  8p2e10  12167  5t5e25  12190  6t6e36  12195  8t6e48  12206  nn0uz  12269  nnuz  12270  xaddcom  12623  x2times  12682  ioomax  12801  iccmax  12802  ioopos  12803  ioorp  12804  prunioo  12857  fseq1p1m1  12971  fzo13pr  13111  fzo0to2pr  13112  fzo0to3tp  13113  om2uzrdg  13314  fzennn  13326  irec  13554  sq10e99m1  13615  facnn  13625  fac0  13626  faclbnd2  13641  faclbnd4lem1  13643  hashfun  13788  hashbclem  13800  hashf1lem1  13803  hashf1lem2  13804  fz1isolem  13809  swrdccatin1  14077  swrdccat3blem  14091  s1co  14185  s2eq2s1eq  14288  s3eqs2s1eq  14290  ofs2  14321  dfid5  14376  dfid6  14377  fsumrev2  15127  fsumparts  15151  fsumiun  15166  isumnn0nn  15187  harmonic  15204  fprod2d  15325  bpoly2  15401  bpoly3  15402  bpoly4  15403  ege2le3  15433  cos1bnd  15530  efieq1re  15542  eirrlem  15547  qnnen  15556  cpnnen  15572  ruclem6  15578  3dvds  15670  pwp1fsum  15732  m1bits  15779  algrp1  15908  phiprmpw  16103  prmreclem4  16245  4sqlem11  16281  4sqlem19  16289  dec5dvds  16390  decsplit1  16408  5prm  16432  7prm  16434  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  strle1  16582  grpbasex  16603  grpplusgx  16604  quslem  16806  xpsrnbas  16834  acsfn1  16922  acsfn2  16924  comfffval2  16961  xpchomfval  17419  xpccofval  17422  1stfval  17431  2ndfval  17434  oduleg  17732  ismgmid  17865  grpinvfvi  18086  gaorb  18377  cntri  18401  cntrsubgnsg  18411  cntrnsg  18412  oppglem  18418  oppgcntr  18433  gsumwrev  18434  symgbas  18438  symgga  18466  cayleylem1  18471  psgnunilem2  18554  efgval2  18781  efgredlemc  18802  efgcpbllema  18811  frgpnabllem1  18924  gsumzaddlem  18972  mgplem  19175  opprlem  19309  oppr0  19314  opprneg  19316  rmodislmod  19633  rlmscaf  19911  mplbas  20139  mpladd  20152  mplmul  20153  mplvsca2  20156  ressmplbas2  20166  ltbwe  20183  evlslem4  20218  psr1bas2  20288  ply1bas  20293  ply1assa  20297  mplplusg  20318  mplmulr  20319  psr1plusg  20320  psr1vsca  20321  psr1mulr  20322  ply1plusg  20323  ply1vsca  20324  ply1mulr  20325  ply1mpl0  20353  ply1mpl1  20355  coe1mul  20368  xrsds  20518  gsumfsum  20542  zringunit  20565  cnmsgngrp  20653  psgnfix2  20673  relt  20689  ocv0  20751  thlle  20771  thlleval  20772  dsmmval2  20810  frlmip  20852  matgsum  20976  smadiadetglem1  21210  indistpsx  21548  iuncld  21583  tgrest  21697  resstopn  21724  leordtval2  21750  xkouni  22137  ptclsg  22153  ptuncnv  22345  ptunhmeo  22346  alexsubALTlem4  22588  tsmsf1o  22682  ucnimalem  22818  ressxms  23064  uniretop  23300  cnfldtopn  23319  xrtgioo  23343  zcld  23350  icccmp  23362  xrge0gsumle  23370  xrge0tsms  23371  metnrmlem3  23398  fsum2cn  23408  cnmpopc  23461  oprpiece1res1  23484  oprpiece1res2  23485  evth  23492  evth2  23493  om1opn  23569  pi1xfrf  23586  pi1xfrcnv  23590  pi1cof  23592  clsocv  23782  cncmet  23854  cnflduss  23888  rrxprds  23921  ehlbase  23947  ismbl  24056  shftmbl  24068  ioorinv  24106  itg1addlem4  24229  itg2cnlem1  24291  itg0  24309  itgss3  24344  ditgneg  24384  limcdif  24403  limciun  24421  dvexp  24479  dvef  24506  dvcnvrelem2  24544  ftc1  24568  aannenlem2  24847  dvradcnv  24938  pserdvlem2  24945  reefgim  24967  cospi  24987  sincos6thpi  25030  tanregt0  25050  dflog2  25071  logfac  25111  dvlog  25161  cxpexp  25178  cxpmul2  25199  cxpsqrt  25213  dvsqrt  25250  dvcnsqrt  25252  cxpcn2  25254  isosctrlem2  25324  1cubrlem  25346  1cubr  25347  quart1lem  25360  atancj  25415  atanlogaddlem  25418  atansopn  25437  leibpilem2  25447  log2cnv  25450  log2ublem3  25454  birthdaylem1  25457  birthdaylem2  25458  birthday  25460  dfarea  25466  lgamgulmlem5  25538  lgambdd  25542  ftalem3  25580  basellem2  25587  ppiprm  25656  ppinprm  25657  chtprm  25658  chtnprm  25659  ppi2  25675  ppi3  25676  ppiub  25708  chtub  25716  bclbnd  25784  bposlem8  25795  lgsdilem  25828  lgsdir2lem2  25830  lgsquadlem2  25885  lgsquad2lem2  25889  2lgsoddprmlem3c  25916  rplogsum  26031  mulog2sumlem2  26039  pnt2  26117  istrkg2ld  26174  axsegconlem9  26639  ax5seglem7  26649  iedgedg  26763  uspgrf1oedg  26886  nbgrcl  27045  nbgrnvtx0  27049  rusgrprc  27300  wlkiswwlks2lem4  27578  wlkiswwlks2lem5  27579  wwlksnfiOLD  27613  clwwlkvbij  27820  konigsbergumgr  27958  ex-pw  28136  ex-xp  28143  ex-rn  28147  nvvop  28314  nvm  28346  cnims  28398  ip0i  28530  ip1ilem  28531  ipdirilem  28534  ipasslem10  28544  h2hva  28679  h2hsm  28680  h2hvs  28682  axhfvadd-zf  28687  axhvcom-zf  28688  axhvass-zf  28689  axhv0cl-zf  28690  axhvaddid-zf  28691  axhfvmul-zf  28692  axhvmulid-zf  28693  axhvmulass-zf  28694  axhvdistr1-zf  28695  axhvdistr2-zf  28696  axhvmul0-zf  28697  axhfi-zf  28698  axhis1-zf  28699  axhis2-zf  28700  axhis3-zf  28701  axhis4-zf  28702  axhcompl-zf  28703  normlem0  28814  normlem1  28815  normlem2  28816  normlem4  28818  normlem9  28823  bcseqi  28825  dfhnorm2  28827  norm3difi  28852  normpari  28859  normpar2i  28861  polid2i  28862  polidi  28863  hhba  28872  hhims  28877  hhims2  28878  hhsssh  28974  hhssims  28979  hhssims2  28980  shsval3i  29093  dfch2  29112  cmcm2i  29298  fh2  29324  qlaxr3i  29341  spansnji  29351  pjcji  29389  ho0val  29455  df0op2  29457  hosd1i  29527  hosd2i  29528  eigorthi  29542  hhlnoi  29605  hhnmoi  29606  hhbloi  29607  bra0  29655  nmop0  29691  nmfn0  29692  lnopeq0lem1  29710  lnopunilem1  29715  lnophmlem2  29722  nmopcoadji  29806  pjhmopidm  29888  cvmdi  30029  cdj3lem3  30143  cdj3lem3b  30145  abrexdomjm  30195  uniin1  30231  uniin2  30232  iundifdifd  30242  iundifdif  30243  mpomptxf  30354  df1stres  30366  df2ndres  30367  fcobijfs  30386  resf1o  30393  fpwrelmapffslem  30395  dpval3  30498  dp3mul10  30502  dpadd2  30514  dpmul4  30518  xrslt  30591  xrsclat  30595  xrge0tsmsd  30620  gsumle  30653  cycpmco2lem7  30702  cycpmconjv  30712  cycpmrn  30713  xrge0slmod  30845  rgmoddim  30908  circtopn  31001  tpr2rico  31055  xrge0mulc1cn  31084  lmxrge0  31095  esumpfinvallem  31233  esumcocn  31239  hasheuni  31244  esumcvg  31245  rossros  31339  measinblem  31379  aean  31403  sxbrsigalem3  31430  dya2iocival  31431  dya2iocucvr  31442  sxbrsigalem1  31443  sxbrsigalem2  31444  sxbrsigalem5  31446  sxbrsiga  31448  fiunelcarsg  31474  eulerpartlem1  31525  eulerpartgbij  31530  fibp1  31559  coinfliplem  31636  coinflipprob  31637  ballotlemfval  31647  ballotth  31695  sgnneg  31698  plymulx  31718  circlemethhgt  31814  hgt750lem2  31823  bnj1400  32007  bnj66  32032  bnj882  32098  lfuhgr  32262  derang0  32314  subfacp1lem1  32324  subfacp1lem6  32330  kur14lem7  32357  cvmsss2  32419  cvmliftlem8  32437  cvmliftlem10  32439  satfv1lem  32507  msubfval  32669  quad3  32811  bcprod  32868  bccolsum  32869  faclim  32876  dftrpred2  32956  bdayfo  33080  pprodcnveq  33242  dfon4  33252  fobigcup  33259  dfiota3  33282  dfrecs2  33309  dfrdg4  33310  dfint3  33311  rankeq1o  33530  refssfne  33604  ssoninhaus  33694  onint1  33695  bj-rababw  34095  bj-inrab3  34145  dissneq  34505  dffinxpf  34549  finxpreclem4  34558  wl-dfrabsb  34743  rabiun  34747  ptrest  34773  poimirlem3  34777  poimirlem4  34778  poimirlem13  34787  poimirlem16  34790  poimirlem22  34796  poimirlem26  34800  poimirlem27  34801  poimirlem30  34804  cnambfre  34822  ftc1anclem8  34856  fnopabco  34881  abrexdom  34888  cncfres  34926  scottexf  35329  scott0f  35330  inres2  35389  dfres4  35433  xrnres  35532  xrnres2  35533  dfcoss2  35543  dfcoss4  35545  1cossres  35556  dmcoss2  35576  1cosscnvxrn  35597  dfeqvrels2  35705  dfcoeleqvrels  35738  redundss3  35745  dffunsALTV5  35802  cdleme3d  37249  cdleme7a  37261  cdleme31sdnN  37405  cdlemk45  37965  imaopab  38999  dfqs2  39002  dfqs3  39003  decaddcom  39050  nn0expgcd  39064  sn-00idlem2  39109  mapfzcons  39193  eldioph4b  39288  diophren  39290  pwssplit4  39569  pwfi2f1o  39576  frlmpwfi  39578  mendplusgfval  39665  mendmulrfval  39667  mendvscafval  39670  idomodle  39676  cytpval  39689  arearect  39702  tr3dom  39774  alephiso2  39797  alephiso3  39798  relintab  39823  dfid7  39852  cnvrcl0  39865  dfrtrcl5  39869  dfrcl3  39900  dfrcl4  39901  comptiunov2i  39931  corcltrcl  39964  neicvgnvo  40345  inductionexd  40385  mnuprdlem2  40489  nznngen  40528  hashnzfz2  40533  lhe4.4ex1a  40541  dvradcnv2  40559  binomcxplemrat  40562  binomcxplemnotnn0  40568  refsum2cnlem1  41174  fiiuncl  41207  iccdifprioo  41672  lptre2pt  41801  limclner  41812  stoweidlem13  42179  stoweidlem32  42198  stoweidlem62  42228  wallispi2lem2  42238  stirlinglem14  42253  dirkertrigeqlem1  42264  dirkercncflem4  42272  fourierdlem42  42315  fourierdlem73  42345  fourierdlem81  42353  fourierdlem92  42364  fourierdlem103  42375  fourierdlem104  42376  fouriercnp  42392  fouriersw  42397  sge0tsms  42543  sge0iunmptlemfi  42576  ovolval5lem3  42817  cnfsmf  42898  rnfdmpr  43361  fvmptrabdm  43373  m11nprm  43613  opoeALTV  43695  nfermltl8rev  43754  sbgoldbo  43799  evengpop3  43810  efmndbas  43940  smndex2dnrinv  43985  cznabel  44123  cznrng  44124  mpomptx2  44281  2sphere  44634  itscnhlinecirc02plem3  44669  inlinecirc02p  44672  amgmlemALT  44802
  Copyright terms: Public domain W3C validator