HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eqtr4 1490
Description: An equality transitivity inference.
Hypotheses
Ref Expression
eqtr4.1 |- A = B
eqtr4.2 |- C = B
Assertion
Ref Expression
eqtr4 |- A = C
Proof of Theorem eqtr4
StepHypRef Expression
1 eqtr4.1 . 2 |- A = B
2 eqtr4.2 . . 3 |- C = B
32eqcomi 1471 . 2 |- B = C
41, 3eqtr 1487 1 |- A = C
Colors of variables: wff set class
Syntax hints:   = wceq 953
This theorem is referenced by:  3eqtr2 1493  3eqtr4 1497  3eqtr4r 1498  dfin5 2042  dfdif2 2046  difeqri 2150  unrab 2260  inrab 2261  inrab2 2262  difrab 2263  pw0 2459  dfint2 2525  uniiun 2591  intiin 2592  0iin 2596  iunun 2603  dfid3 2826  xpundi 3215  xpundir 3216  rnopab2 3340  resopab 3379  imaun2 3447  cnvcnv 3472  cnvcnv2 3473  cnvcnvres 3480  rnco2 3489  dmco2 3490  abrexex2 3856  dmoprab 3987  fnoprval 4002  oprabval4g 4016  1stval2 4073  2ndval2 4074  xp2 4089  df1st2 4110  df2nd2 4111  df2o2 4125  o1p1e2 4159  oarec 4180  fvopabf4 4324  map0e 4326  ixpconst 4336  ixp0x 4343  1sdom2 4505  abfii4 4538  pwfi 4545  infeq5 4593  rankpr 4664  rankelun 4679  rankelop 4681  kmlem11 4747  cf0 4882  ltexpq 5052  halfpq 5054  genpdm 5077  prlem936a 5125  m1p1sr 5173  m1m1sr 5174  mappsrpr 5190  dfcnqs 5234  ltreci 5826  lt2msq 5829  2p2e4 5948  3p2e5 5954  3p3e6 5955  4p2e6 5956  4p3e7 5957  4p4e8 5958  5p2e7 5959  5p3e8 5960  5p4e9 5961  5p5e10 5962  6p2e8 5963  6p3e9 5964  6p4e10 5965  7p2e9 5966  7p3e10 5967  8p2e10 5968  nnzrab 6104  nn0zrab 6105  seq1suclem 6253  ioomax 6325  ioopos 6326  ioorp 6327  nn0uz 6370  nnuz 6371  seq1seqz 6473  seq0seqz 6474  binom2aOLD 6576  discrlem1 6586  sqrval 6601  sqrlem11 6613  irec 6661  crulem 6666  crmul 6671  cjcj 6713  cjreb 6716  cjmul 6724  addcj 6733  recvalz 6825  facnnt 6870  faclbnd2 6883  faclbnd4lem1 6885  bcpasc2 6905  serzclim0 7046  isumnn0nn 7142  isumclt 7144  geolimilem 7170  geolim1i 7173  0.999... 7181  cncfval 7199  isupivth 7225  ivth2OLD 7234  efclt 7254  efaddlem12 7291  efaddlem20 7299  efaddlem22 7301  eirrlem3 7332  efsep 7337  ef4p 7340  sinadd 7393  cos2tOLD 7406  cos1bnd 7416  cos2bnd 7417  ruclem17 7469  infxpidmlem9 7503  alephsuc3 7527  cnconst 7719  cncfmet1 7845  xplm 7909  opr1scn 7914  ringsn 8100  nvvop 8166  nvvc 8174  vsfval 8194  nvm 8202  cnims 8269  sqcn 8270  ip1cnilem4 8310  ip1cnilem6 8312  ip0i 8415  ip1ilem 8416  ip2i 8418  ipasslem6 8426  ipasslem7 8427  ipasslem10 8430  minveclem27 8502  pilem3 8592  sinhalfpilem 8598  cospi 8601  sincos6thpi 8628  dflog2 8674  h2hva 8782  h2hsm 8783  h2hvs 8785  h2hcau 8788  h2hlm 8789  hvsubass 8843  normlem0 8896  normlem1 8897  normlem2 8898  normlem4 8900  normlem9 8905  bcseq 8907  dfhnorm2 8909  normpar 8942  normpar2 8944  polid2 8945  polid 8946  hhba 8955  hhims 8960  hhims2 8961  hhsssh 9059  ocvalt 9069  projlem3 9104  pjthlem1 9134  pjthlem5 9138  pjthlem6 9139  spanvalt 9214  hsupval2t 9215  sshjvalt 9235  sshjval3t 9241  shsumval3 9276  hosmvalt 9428  hommvalt 9429  hodmvalt 9430  hfsmvalt 9431  hfmmvalt 9432  cmcm2 9453  fh2t 9479  qlaxr3 9494  pjcj 9546  ho0valt 9593  df0op2 9595  hosd2 9666  eigorth 9680  dfbdop2 9703  hhnmo 9744  hhblo 9745  hh0o 9746  nmop0 9826  nmfn0 9827  lnopeq0lem1 9845  lnophmlem2 9857  nmopcoadj 9948  cvmd 10159  cdj3lem3 10270  cdj3lem3b 10272  ghomgrpilem2 10291  cayleylem2 10317  infi1 10347  cmpbva 10360  hmeogrp 10425  trnij 10481  stoi 10483  jdmo 10555
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462
Copyright terms: Public domain