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

Theorem eqtr4i 2447
Description: An equality transitivity inference. (Contributed by NM, 26-May-1993.)
Hypotheses
Ref Expression
eqtr4i.1  |-  A  =  B
eqtr4i.2  |-  C  =  B
Assertion
Ref Expression
eqtr4i  |-  A  =  C

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2  |-  A  =  B
2 eqtr4i.2 . . 3  |-  C  =  B
32eqcomi 2431 . 2  |-  B  =  C
41, 3eqtri 2444 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-cleq 2415
This theorem is referenced by:  3eqtr2i  2450  3eqtr2ri  2451  3eqtr4i  2454  3eqtr4ri  2455  rabab  3035  cbvralcsf  3363  cbvrabcsf  3366  dfin5  3380  dfdif2  3381  uneqin  3660  unrab  3680  inrab  3681  inrab2  3682  difrab  3683  dfrab3ss  3687  rabun2  3688  rabxm  3721  elnelun  3724  difidALT  3802  difdifdir  3821  dfif3  3861  dfif5  3863  rabsnif  4005  tpidm  4040  ssunpr  4098  sstp  4100  dfint2  4193  iunrab  4282  uniiun  4288  intiin  4289  0iin  4293  mptv  4453  dfepfr  4774  epfrc  4775  xpundi  4842  xpundir  4843  csbcnv  4973  resiun2  5079  resopab  5106  opabresid  5113  dffr3  5156  dfse2  5157  cnvun  5196  imaundir  5204  imainrect  5233  cnvcnv2  5244  cnvcnvres  5254  dmtpop  5267  rnsnopg  5270  rnco2  5297  dmco  5298  co01  5305  unidmrn  5321  dfdm2  5323  predidm  5357  tz6.26  5366  dfmpt3  5652  mptun  5663  funcocnv2  5791  dffv2  5891  fnasrn  6022  fpr  6024  fmptap  6039  riotav  6209  dmoprab  6328  rnoprab2  6331  mpt2v  6337  mpt2mptx  6338  abrexex2g  6721  abrexex2  6725  1stval2  6761  2ndval2  6762  fo1st  6764  fo2nd  6765  xp2  6779  dfoprab4f  6802  offval22  6823  fmpt2co  6827  tposmpt2  6958  tposconst  6959  recsfval  7047  rdgsucmpt2  7096  frsucmpt2  7105  df2o3  7143  o1p1e2  7190  oarec  7211  omopthlem2  7305  ecqs  7375  qliftf  7399  erovlem  7407  mapsnf1o3  7468  ixp0x  7498  omf1o  7621  xpf1o  7680  mapunen  7687  enp1ilem  7751  pwfi  7815  marypha1lem  7893  marypha2lem4  7898  dfoi  7972  infeq5i  8087  oemapso  8132  cantnflem1  8139  rankelop  8290  leweon  8387  r0weon  8388  kmlem11  8534  infcda1  8567  ackbij1lem16  8609  cf0  8625  cfsmolem  8644  alephsuc3  8949  fpwwe  9015  canthp1lem1  9021  wuncval2  9116  prlem936  9416  m1p1sr  9460  m1m1sr  9461  dfcnqs  9510  ssxr  9647  mul02lem2  9754  addid1  9757  3m1e2  10670  2p2e4  10671  3p2e5  10686  3p3e6  10687  4p2e6  10688  4p3e7  10689  4p4e8  10690  5p2e7  10691  5p3e8  10692  5p4e9  10693  5p5e10  10694  6p2e8  10695  6p3e9  10696  6p4e10  10697  7p2e9  10698  7p3e10  10699  8p2e10  10700  nnzrab  10909  nn0zrab  10910  dec0u  11010  dec0h  11011  decsuc  11018  decsucc  11022  numma  11026  decma  11033  decmac  11034  decma2c  11035  decadd  11036  decaddc  11037  decmul1c  11042  decmul2c  11043  5t5e25  11071  6t6e36  11076  8t6e48  11087  nn0uz  11137  nnuz  11138  xaddcom  11475  x2times  11529  ioomax  11653  iccmax  11654  ioopos  11655  ioorp  11656  prunioo  11705  fseq1p1m1  11812  fzo13pr  11940  fzo0to2pr  11941  fzo0to3tp  11942  om2uzrdg  12113  fzennn  12124  irec  12317  facnn  12404  fac0  12405  faclbnd2  12419  faclbnd4lem1  12421  hashfun  12550  hashbclem  12556  hashf1lem1  12559  hashf1lem2  12560  fz1isolem  12565  swrdccatin1  12778  swrdccat3blem  12790  s1co  12869  s2eq2s1eq  12955  dfid5  13027  dfid6  13028  fsumrev2  13779  fsumparts  13802  fsumiun  13817  isumnn0nn  13836  harmonic  13853  0.999...  13873  fprod2d  13971  bpoly2  14046  bpoly3  14047  bpoly4  14048  ege2le3  14080  cos1bnd  14177  efieq1re  14189  eirrlem  14192  qnnen  14202  cpnnen  14217  ruclem6  14223  3dvds  14305  m1bits  14350  algrp1  14469  phiprmpw  14660  prmreclem4  14799  4sqlem11  14835  4sqlem19  14849  dec5dvds  14972  decsplit1  14990  5prm  15016  7prm  15018  1259lem2  15039  1259lem3  15040  1259lem4  15041  1259lem5  15042  1259prm  15043  2503lem1  15044  2503lem2  15045  2503lem3  15046  2503prm  15047  4001lem1  15048  4001lem2  15049  4001lem3  15050  4001lem4  15051  4001prm  15052  ndxid  15078  strle1  15157  grpbasex  15176  grpplusgx  15177  quslem  15385  xpslem  15415  acsfn1  15503  acsfn2  15505  comfffval2  15542  xpchomfval  16000  xpccofval  16003  1stfval  16012  2ndfval  16015  oduleg  16314  ismgmid  16443  grpinvfvi  16643  gaorb  16897  cntri  16920  cntrsubgnsg  16930  cntrnsg  16931  oppglem  16937  oppgcntr  16952  gsumwrev  16953  symgbas  16957  symgga  16983  cayleylem1  16989  psgnunilem2  17072  efgval2  17310  efgredlemc  17331  efgcpbllema  17340  frgpnabllem1  17445  gsumzaddlem  17490  mgplem  17664  opprlem  17792  oppr0  17797  opprneg  17799  rlmscaf  18367  mplbas  18589  mpladd  18602  mplmul  18603  mplvsca2  18606  ressmplbas2  18615  ltbwe  18632  evlslem4  18667  psr1bas2  18719  ply1bas  18724  ply1assa  18728  mplplusg  18749  mplmulr  18750  psr1plusg  18751  psr1vsca  18752  psr1mulr  18753  ply1plusg  18754  ply1vsca  18755  ply1mulr  18756  ply1mpl0  18784  ply1mpl1  18786  coe1mul  18799  xrsds  18947  gsumfsum  18970  zringunit  18997  cnmsgngrp  19082  psgnfix2  19102  relt  19118  ocv0  19175  thlle  19195  thlleval  19196  dsmmval2  19234  frlmip  19271  matgsum  19397  smadiadetglem1  19631  indistpsx  19960  iuncld  19995  tgrest  20110  resstopn  20137  leordtval2  20163  xkouni  20549  ptclsg  20565  ptuncnv  20757  ptunhmeo  20758  alexsubALTlem4  21000  tsmsf1o  21094  ucnimalem  21230  ressxms  21475  uniretop  21718  cnfldtopn  21737  xrtgioo  21759  zcld  21766  icccmp  21778  xrge0gsumle  21786  xrge0tsms  21787  metnrmlem3  21813  metnrmlem3OLD  21828  fsum2cn  21838  cnmpt2pc  21891  oprpiece1res1  21914  oprpiece1res2  21915  evth  21922  evth2  21923  om1opn  22002  pi1xfrf  22019  pi1xfrcnv  22023  pi1cof  22025  clsocv  22156  cncmet  22225  cnflduss  22258  rrxprds  22283  ehlbase  22300  ismbl  22415  shftmbl  22427  ioorinv  22463  ioorinvOLD  22468  itg1addlem4  22592  itg2cnlem1  22654  iblitg  22661  itg0  22672  itgss3  22707  ditgneg  22747  limcdif  22766  limciun  22784  dvexp  22842  dvef  22867  dvcnvrelem2  22905  ftc1  22929  plyremlem  23192  aannenlem2  23220  taylply2  23258  dvradcnv  23311  pserdvlem2  23318  reefgim  23340  cospi  23362  sincos6thpi  23405  tanregt0  23423  dflog2  23445  logfac  23485  dvlog  23531  cxpexp  23548  cxpmul2  23569  cxpsqrt  23583  dvsqrt  23617  dvcnsqrt  23619  cxpcn2  23621  ang180lem2  23674  isosctrlem2  23683  1cubrlem  23702  1cubr  23703  quart1lem  23716  atancj  23771  atanlogaddlem  23774  atansopn  23793  leibpilem2  23802  log2cnv  23805  log2ublem3  23809  birthdaylem1  23812  birthdaylem2  23813  birthday  23815  dfarea  23821  lgamgulmlem5  23893  lgambdd  23897  wilthlem2  23929  ftalem3  23934  ftalem7  23940  basellem2  23943  ppiprm  24013  ppinprm  24014  chtprm  24015  chtnprm  24016  ppi2  24032  ppi3  24033  ppiub  24067  chtub  24075  bclbnd  24143  bposlem8  24154  lgsdilem  24185  lgsdir2lem1  24186  lgsdir2lem2  24187  lgsdir2lem3  24188  lgsquadlem2  24218  lgsquad2lem2  24222  rplogsum  24300  mulog2sumlem2  24308  pnt2  24386  istrkg2ld  24443  axsegconlem9  24890  ax5seglem7  24900  usgrares1  25073  cusgrares  25135  wwlknprop  25349  wwlknfi  25401  wlknwwlknvbij  25403  clwwlkvbij  25464  eupath2lem3  25642  konigsberg  25650  ex-pw  25814  ex-xp  25821  ex-rn  25825  ablosn  26010  efghgrpOLD  26036  nvvop  26163  nvm  26197  cnims  26264  ip0i  26401  ip1ilem  26402  ipdirilem  26405  ipasslem10  26415  h2hva  26562  h2hsm  26563  h2hvs  26565  axhfvadd-zf  26570  axhvcom-zf  26571  axhvass-zf  26572  axhv0cl-zf  26573  axhvaddid-zf  26574  axhfvmul-zf  26575  axhvmulid-zf  26576  axhvmulass-zf  26577  axhvdistr1-zf  26578  axhvdistr2-zf  26579  axhvmul0-zf  26580  axhfi-zf  26581  axhis1-zf  26582  axhis2-zf  26583  axhis3-zf  26584  axhis4-zf  26585  axhcompl-zf  26586  normlem0  26697  normlem1  26698  normlem2  26699  normlem4  26701  normlem9  26706  bcseqi  26708  dfhnorm2  26710  norm3difi  26735  normpari  26742  normpar2i  26744  polid2i  26745  polidi  26746  hhba  26755  hhims  26760  hhims2  26761  hhsssh  26855  hhssims  26861  hhssims2  26862  shsval3i  26976  dfch2  26995  cmcm2i  27181  fh2  27207  qlaxr3i  27224  spansnji  27234  pjcji  27272  ho0val  27338  df0op2  27340  hosd1i  27410  hosd2i  27411  eigorthi  27425  hhlnoi  27488  hhnmoi  27489  hhbloi  27490  bra0  27538  nmop0  27574  nmfn0  27575  lnopeq0lem1  27593  lnopunilem1  27598  lnophmlem2  27605  nmopcoadji  27689  pjhmopidm  27771  cvmdi  27912  cdj3lem3  28026  cdj3lem3b  28028  abrexdomjm  28077  uniin1  28103  uniin2  28104  iundifdifd  28116  iundifdif  28117  mpt2mptxf  28219  df1stres  28223  df2ndres  28224  fcobijfs  28254  resf1o  28258  fpwrelmapffslem  28260  xrslt  28382  xrsclat  28386  gsumle  28486  xrge0tsmsd  28493  xrge0slmod  28552  fimaproj  28605  circtopn  28609  tpr2rico  28663  xrge0mulc1cn  28692  lmxrge0  28703  esumpfinvallem  28840  esumcocn  28846  hasheuni  28851  esumcvg  28852  rossros  28947  measinblem  28987  aean  29012  sxbrsigalem3  29039  dya2iocival  29040  dya2iocucvr  29051  sxbrsigalem1  29052  sxbrsigalem2  29053  sxbrsigalem5  29055  sxbrsiga  29057  fiunelcarsg  29093  eulerpartlem1  29145  eulerpartgbij  29150  fibp1  29179  coinfliplem  29256  coinflipprob  29257  ballotlemfval  29267  ballotth  29315  ballotthOLD  29353  sgnneg  29356  ofs2  29378  plymulx  29382  bnj1400  29592  bnj66  29616  bnj882  29682  derang0  29837  subfacp1lem1  29847  subfacp1lem6  29853  kur14lem7  29880  cvmsss2  29942  cvmliftlem8  29960  cvmliftlem10  29962  msubfval  30107  quad3  30247  ghomgrpilem2  30249  bcprod  30318  bccolsum  30319  faclim  30326  dftrpred2  30404  bdayfo  30506  pprodcnveq  30592  dfon4  30602  fobigcup  30609  dfiota3  30632  dfrecs2  30659  dfrdg4  30660  dfint3  30661  rankeq1o  30880  refssfne  30956  ssoninhaus  31050  onint1  31051  bj-rababwv  31383  bj-inrab3  31438  rnmptsn  31638  dissneq  31644  dffinxpf  31678  finxpreclem4  31687  rabiun  31827  ptrest  31840  poimirlem3  31844  poimirlem4  31845  poimirlem13  31854  poimirlem16  31857  poimirlem22  31863  poimirlem25  31866  poimirlem26  31867  poimirlem27  31868  poimirlem30  31871  cnambfre  31890  ftc1anclem8  31925  fnopabco  31950  abrexdom  31958  cncfres  31998  scottexf  32312  scott0f  32313  cdleme3d  33703  cdleme7a  33715  cdleme31sdnN  33860  cdlemk45  34420  mapfzcons  35464  eldioph4b  35560  diophren  35562  pwssplit4  35854  pwfi2f1o  35861  frlmpwfi  35863  mendplusgfval  35958  mendmulrfval  35960  mendvscafval  35963  idomodle  35977  cytpval  35993  arearect  36007  relintab  36096  dfid7  36126  cnvrcl0  36139  dfrtrcl5  36143  dfrcl3  36174  dfrcl4  36175  comptiunov2i  36205  corcltrcl  36238  inductionexd  36500  nznngen  36572  hashnzfz2  36577  lhe4.4ex1a  36585  dvradcnv2  36603  binomcxplemrat  36606  binomcxplemnotnn0  36612  compne  36700  refsum2cnlem1  37268  fiiuncl  37316  rnmptc  37334  iccdifprioo  37503  lptre2pt  37597  limclner  37609  stoweidlem13  37750  stoweidlem32  37770  stoweidlem62  37800  stoweidlem62OLD  37801  wallispi2lem2  37811  stirlinglem14  37826  dirkertrigeqlem1  37837  dirkercncflem4  37845  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem73  37920  fourierdlem81  37928  fourierdlem92  37939  fourierdlem103  37950  fourierdlem104  37951  fouriercnp  37967  fouriersw  37972  sge0tsms  38067  sge0iunmptlemfi  38100  opoeALTV  38619  evengpop3  38700  rnfdmpr  38815  nbgrnvtx0  39139  nbgrel  39140  cznabel  39541  cznrng  39542  mpt2mptx2  39703
  Copyright terms: Public domain W3C validator