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

Theorem eqtr4i 2427
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-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 2408 . 2  |-  B  =  C
41, 3eqtri 2424 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  3eqtr2i  2430  3eqtr2ri  2431  3eqtr4i  2434  3eqtr4ri  2435  rabab  2933  cbvralcsf  3271  cbvrabcsf  3274  dfin5  3288  dfdif2  3289  uneqin  3552  unrab  3572  inrab  3573  inrab2  3574  difrab  3575  dfrab3ss  3579  rabun2  3580  rabxm  3610  difidALT  3657  difdifdir  3675  dfif3  3709  dfif5  3711  tpidm  3868  ssunpr  3921  sstp  3923  dfint2  4012  iunrab  4098  uniiun  4104  intiin  4105  0iin  4109  mptv  4261  dfepfr  4527  epfrc  4528  xpundi  4889  xpundir  4890  resiun2  5125  resopab  5146  opabresid  5153  dffr3  5195  dfse2  5196  cnvun  5236  imaundir  5244  imainrect  5271  cnvcnv2  5283  cnvcnvres  5292  dmtpop  5305  rnsnopg  5308  rnco2  5336  dmco  5337  co01  5343  unidmrn  5358  dfdm2  5360  dfmpt3  5526  mptun  5534  funcocnv2  5659  dffv2  5755  fnasrn  5871  fpr  5873  fmptap  5882  abrexex2g  5947  abrexex2  5960  dmoprab  6113  rnoprab2  6116  mpt2v  6122  mpt2mptx  6123  1stval2  6323  2ndval2  6324  fo1st  6325  fo2nd  6326  xp2  6343  dfoprab4f  6364  fmpt2co  6389  tposmpt2  6475  riotav  6513  cbvriota  6519  recsfval  6601  rdgsucmpt2  6647  frsucmpt2  6656  df2o3  6696  o1p1e2  6743  oarec  6764  omopthlem2  6858  ecqs  6927  qliftf  6951  erovlem  6959  mapsnf1o3  7021  ixp0x  7049  omf1o  7170  xpf1o  7228  mapunen  7235  enp1ilem  7301  pwfi  7360  marypha1lem  7396  marypha2lem4  7401  dfoi  7436  infeq5i  7547  oemapso  7594  cantnflem1  7601  rankelop  7756  leweon  7849  r0weon  7850  kmlem11  7996  infcda1  8029  ackbij1lem16  8071  cf0  8087  cfsmolem  8106  alephsuc3  8411  fpwwe  8477  canthp1lem1  8483  wuncval2  8578  prlem936  8880  m1p1sr  8923  m1m1sr  8924  dfcnqs  8973  ssxr  9101  mul02lem2  9199  addid1  9202  3m1e2  10052  3m1e2OLD  10053  2p2e4  10054  3p2e5  10067  3p3e6  10068  4p2e6  10069  4p3e7  10070  4p4e8  10071  5p2e7  10072  5p3e8  10073  5p4e9  10074  5p5e10  10075  6p2e8  10076  6p3e9  10077  6p4e10  10078  7p2e9  10079  7p3e10  10080  8p2e10  10081  nn0supp  10229  nnzrab  10265  nn0zrab  10266  dec0u  10353  dec0h  10354  decsuc  10361  decsucc  10365  numma  10369  decma  10376  decmac  10377  decma2c  10378  decadd  10379  decaddc  10380  decmul1c  10385  decmul2c  10386  5t5e25  10414  6t6e36  10419  8t6e48  10430  nn0uz  10476  nnuz  10477  xaddcom  10780  x2times  10834  ioomax  10941  iccmax  10942  ioopos  10943  ioorp  10944  prunioo  10981  fseq1p1m1  11077  fzo0to2pr  11139  fzo0to3tp  11140  om2uzrdg  11251  fzennn  11262  irec  11435  binom2aiOLD  11446  facnn  11523  fac0  11524  faclbnd2  11537  faclbnd4lem1  11539  hashfun  11655  hashbclem  11656  hashf1lem1  11659  hashf1lem2  11660  fz1isolem  11665  s1co  11757  fsumrev2  12520  fsumparts  12540  fsumiun  12555  isumnn0nn  12577  harmonic  12593  0.999...  12613  ege2le3  12647  cos1bnd  12743  efieq1re  12755  eirrlem  12758  qnnen  12768  cpnnen  12783  ruclem6  12789  3dvds  12867  m1bits  12907  algrp1  13020  phiprmpw  13120  prmreclem4  13242  4sqlem11  13278  4sqlem19  13286  dec5dvds  13355  decsplit1  13373  5prm  13386  7prm  13388  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  ndxid  13445  strle1  13515  grpbasex  13527  grpplusgx  13528  divslem  13723  xpslem  13753  acsfn1  13841  acsfn2  13843  comfffval2  13882  xpchomfval  14231  xpccofval  14234  1stfval  14243  2ndfval  14246  oduleg  14514  grpinvfvi  14801  gaorb  15039  symgbas  15050  symgga  15064  cayleylem1  15065  cntri  15084  cntrsubgnsg  15094  cntrnsg  15095  oppglem  15101  oppgcntr  15116  gsumwrev  15117  efgval2  15311  efgredlemc  15332  efgcpbllema  15341  frgpnabllem1  15439  gsumzaddlem  15481  mgplem  15608  opprlem  15688  oppr0  15693  opprneg  15695  rlmscaf  16234  mplbas  16448  mpladd  16460  mplmul  16461  mplvsca2  16464  ressmplbas2  16473  ltbwe  16488  evlslem4  16519  psr1bas2  16543  ply1bas  16548  ply1assa  16552  mplplusg  16569  mplmulr  16570  psr1plusg  16571  psr1vsca  16572  psr1mulr  16573  ply1plusg  16574  ply1vsca  16575  ply1mulr  16576  ply1mpl0  16604  ply1mpl1  16605  coe1mul  16618  xrsds  16696  zrngunit  16720  gsumfsum  16721  ocv0  16859  thlle  16879  thlleval  16880  indistpsx  17029  iuncld  17064  tgrest  17177  resstopn  17204  leordtval2  17230  xkouni  17584  ptclsg  17600  ptuncnv  17792  ptunhmeo  17793  alexsubALTlem4  18034  tsmsf1o  18127  ucnimalem  18263  ressxms  18508  uniretop  18749  cnfldtopn  18769  xrtgioo  18790  zcld  18797  icccmp  18809  xrge0gsumle  18817  xrge0tsms  18818  metnrmlem3  18844  fsum2cn  18854  cnmpt2pc  18906  oprpiece1res1  18929  oprpiece1res2  18930  evth  18937  evth2  18938  om1opn  19014  pi1xfrf  19031  pi1xfrcnv  19035  pi1cof  19037  clsocv  19157  cncmet  19228  cnflduss  19263  ismbl  19375  shftmbl  19386  ioorinv  19421  itg1addlem4  19544  itg2cnlem1  19606  iblitg  19613  itg0  19624  itgss3  19659  ditgneg  19697  limcdif  19716  limciun  19734  dvexp  19792  dvef  19817  dvcnvrelem2  19855  ftc1  19879  plyremlem  20174  aannenlem2  20199  taylply2  20237  dvradcnv  20290  pserdvlem2  20297  reefgim  20319  cospi  20333  sincos6thpi  20376  tanregt0  20394  dflog2  20411  logfac  20448  dvlog  20495  cxpexp  20512  cxpmul2  20533  cxpsqr  20547  dvsqr  20581  cxpcn2  20583  ang180lem2  20605  isosctrlem2  20616  1cubrlem  20634  1cubr  20635  quart1lem  20648  atancj  20703  atanlogaddlem  20706  atansopn  20725  leibpilem2  20734  log2cnv  20737  log2ublem3  20741  birthdaylem1  20743  birthdaylem2  20744  birthday  20746  dfarea  20752  wilthlem2  20805  ftalem3  20810  ftalem7  20814  basellem2  20817  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  ppi2  20906  ppi3  20907  ppiub  20941  chtub  20949  bclbnd  21017  bposlem8  21028  lgsdilem  21059  lgsdir2lem1  21060  lgsdir2lem2  21061  lgsdir2lem3  21062  lgsquadlem2  21092  lgsquad2lem2  21096  rplogsum  21174  mulog2sumlem2  21182  pnt2  21260  usgrares1  21377  cusgrares  21434  eupath2lem3  21654  konigsberg  21662  ex-pw  21690  ex-xp  21697  ex-rn  21701  ablosn  21888  efghgrp  21914  nvvop  22041  nvm  22075  cnims  22142  ip0i  22279  ip1ilem  22280  ipdirilem  22283  ipasslem10  22293  h2hva  22430  h2hsm  22431  h2hvs  22433  axhfvadd-zf  22438  axhvcom-zf  22439  axhvass-zf  22440  axhv0cl-zf  22441  axhvaddid-zf  22442  axhfvmul-zf  22443  axhvmulid-zf  22444  axhvmulass-zf  22445  axhvdistr1-zf  22446  axhvdistr2-zf  22447  axhvmul0-zf  22448  axhfi-zf  22449  axhis1-zf  22450  axhis2-zf  22451  axhis3-zf  22452  axhis4-zf  22453  axhcompl-zf  22454  normlem0  22564  normlem1  22565  normlem2  22566  normlem4  22568  normlem9  22573  bcseqi  22575  dfhnorm2  22577  norm3difi  22602  normpari  22609  normpar2i  22611  polid2i  22612  polidi  22613  hhba  22622  hhims  22627  hhims2  22628  hhsssh  22722  hhssims  22728  hhssims2  22729  shsval3i  22843  dfch2  22862  cmcm2i  23048  fh2  23074  qlaxr3i  23091  spansnji  23101  pjcji  23139  ho0val  23206  df0op2  23208  hosd1i  23278  hosd2i  23279  eigorthi  23293  hhlnoi  23356  hhnmoi  23357  hhbloi  23358  bra0  23406  nmop0  23442  nmfn0  23443  lnopeq0lem1  23461  lnopunilem1  23466  lnophmlem2  23473  nmopcoadji  23557  pjhmopidm  23639  cvmdi  23780  cdj3lem3  23894  cdj3lem3b  23896  abrexdomjm  23941  iundifdifd  23965  iundifdif  23966  df1stres  24044  df2ndres  24045  xrslt  24151  xrge0tsmsd  24176  relt  24229  tpr2rico  24263  xrge0mulc1cn  24280  lmxrge0  24290  esumpfinvallem  24417  esumcocn  24423  hasheuni  24428  esumcvg  24429  measinblem  24527  aean  24548  sxbrsigalem3  24575  dya2iocival  24576  dya2iocucvr  24587  sxbrsigalem1  24588  sxbrsigalem2  24589  sxbrsigalem5  24591  sxbrsiga  24593  sitgclbn  24610  coinfliplem  24689  coinflipprob  24690  ballotlemfval  24700  ballotth  24748  lgamgulmlem5  24770  lgambdd  24774  derang0  24808  subfacp1lem1  24818  subfacp1lem6  24824  kur14lem7  24851  cvmsss2  24914  cvmliftlem8  24932  cvmliftlem10  24934  ghomgrpilem2  25050  fprod2d  25258  faclim  25313  predidm  25402  tz6.26  25419  dftrpred2  25436  bdayfo  25543  pprodcnveq  25637  dfon4  25647  fobigcup  25654  dfiota3  25676  dfrdg4  25703  axsegconlem9  25768  ax5seglem7  25778  bpoly2  26007  bpoly3  26008  bpoly4  26009  rankeq1o  26016  ssoninhaus  26102  onint1  26103  rabiun2  26139  cnambfre  26154  refssfne  26264  fnopabco  26314  abrexdom  26322  cncfres  26364  mapfzcons  26662  eldioph4b  26762  diophren  26764  rabren3dioph  26766  pwssplit4  27059  dsmmval2  27070  pwfi2f1o  27128  frlmpwfi  27130  psgnunilem2  27286  cnmsgngrp  27304  mendplusgfval  27361  mendmulrfval  27363  mendvscafval  27366  idomodle  27380  cytpval  27396  lhe4.4ex1a  27414  compne  27510  refsum2cnlem1  27575  stoweidlem13  27629  stoweidlem32  27648  stoweidlem62  27678  wallispi2lem2  27688  stirlinglem14  27703  rnfdmpr  27964  swrdccatin1  28016  bnj1400  28913  bnj66  28937  bnj882  29003  cdleme3d  30713  cdleme7a  30725  cdleme31sdnN  30869  cdlemk45  31429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator