Theorem eqtr4 1498

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

Step	Hyp	Ref	Expression
1		eqtr4.1	. 2 |- A = B
2		eqtr4.2	. . 3 |- C = B
3	2	eqcomi 1479	. 2 |- B = C
4	1, 3	eqtr 1495	1 |- A = C

Syntax hints:   = wceq 956

This theorem is referenced by:  3eqtr2 1501  3eqtr4 1505  3eqtr4r 1506  dfin5 2052  dfdif2 2056  difeqri 2160  unrab 2270  inrab 2271  inrab2 2272  difrab 2273  pw0 2468  dfint2 2535  uniiun 2601  intiin 2602  0iin 2606  iunun 2613  dfid3 2836  xpundi 3225  xpundir 3226  rnopab2 3354  resopab 3395  imaun2 3461  cnvcnv 3486  cnvcnv2 3487  cnvcnvres 3494  rnco2 3503  dmco2 3504  abrexex2 3871  dmoprab 4002  fnoprval 4017  oprabval4g 4031  1stval2 4089  2ndval2 4090  xp2 4105  df1st2 4126  df2nd2 4127  df2o2 4141  o1p1e2 4175  oarec 4196  fvopabf4 4340  map0e 4342  ixpconst 4352  ixp0x 4359  1sdom2 4526  abfii4OLD 4564  pwfiOLD 4571  infeq5 4621  rankpr 4692  rankelun 4707  rankelop 4709  kmlem11 4775  cf0 4910  ltexpq 5080  halfpq 5082  genpdm 5105  prlem936a 5153  m1p1sr 5201  m1m1sr 5202  mappsrpr 5218  dfcnqs 5262  ltreci 5878  lt2msq 5881  2p2e4 6001  3p2e5 6007  3p3e6 6008  4p2e6 6009  4p3e7 6010  4p4e8 6011  5p2e7 6012  5p3e8 6013  5p4e9 6014  5p5e10 6015  6p2e8 6016  6p3e9 6017  6p4e10 6018  7p2e9 6019  7p3e10 6020  8p2e10 6021  nnzrab 6157  nn0zrab 6158  seq1suclem 6316  ioomax 6393  ioopos 6394  ioorp 6395  nn0uz 6438  nnuz 6439  seq1seqz 6541  seq0seqz 6542  binom2aOLD 6645  discrlem1 6656  sqrval 6671  sqrlem11 6683  irec 6731  crulem 6736  crmul 6740  cjcj 6778  cjreb 6781  cjmul 6789  addcj 6798  recvalz 6887  facnnt 6933  faclbnd2 6946  faclbnd4lem1 6948  bcpasc2 6967  serzclim0 7109  isumnn0nn 7207  isumclt 7209  geolimilem 7235  geolim1i 7238  0.999... 7246  cncfval 7264  isupivth 7290  efclt 7312  efaddlem12 7349  efaddlem20 7357  efaddlem22 7359  eirrlem3 7391  efsep 7396  ef4p 7399  sinadd 7451  cos2tOLD 7464  cos1bnd 7474  cos2bnd 7475  ruclem17 7526  infxpidmlem9 7560  alephsuc3 7585  cnconst 7780  cncfmet1 7906  xplm 7975  opr1scn 7980  ablsn 8125  ringsn 8163  nvvop 8228  nvvc 8234  vsfval 8254  nvm 8262  cnims 8334  sqcn 8335  ip1cnilem4 8376  ip1cnilem6 8378  ip0i 8484  ip1ilem 8485  ip2i 8487  ipasslem6 8495  ipasslem7 8496  ipasslem10 8499  minveclem27 8571  pilem3 8673  sinhalfpilem 8679  cospi 8682  sincos6thpi 8711  dflog2 8752  h2hva 8843  h2hsm 8844  h2hvs 8846  h2hcau 8849  h2hlm 8850  axhfvadd 8852  axhvcom 8853  axhvass 8854  axhv0cl 8855  axhvaddid 8856  axhfvmul 8857  axhvmulid 8858  axhvmulass 8859  axhvdistr1 8860  axhvdistr2 8861  axhvmul0 8862  axhfi 8863  axhis1 8864  axhis2 8865  axhis3 8866  axhis4 8867  axhcompl 8868  hvsubass 8922  normlem0 8975  normlem1 8976  normlem2 8977  normlem4 8979  normlem9 8984  bcseq 8986  dfhnorm2 8988  normpar 9021  normpar2 9023  polid2 9024  polid 9025  hhba 9034  hhims 9039  hhims2 9040  hhsssh 9139  hhssims 9145  hhssims2 9146  ocvalt 9153  projlem3 9188  pjthlem1 9219  pjthlem5 9223  pjthlem6 9224  spanvalt 9299  hsupval2t 9300  sshjvalt 9320  sshjval3t 9326  shsumval3 9361  hosmvalt 9511  hommvalt 9512  hodmvalt 9513  hfsmvalt 9514  hfmmvalt 9515  cmcm2 9536  fh2t 9562  qlaxr3 9577  pjcj 9629  ho0valt 9676  df0op2 9678  hosd2 9749  eigorth 9763  dfbdop2 9786  hhnmo 9827  hhblo 9828  hh0o 9829  nmop0 9910  nmfn0 9911  lnopeq0lem1 9930  lnophmlem2 9942  nmopcoadj 10034  cvmd 10251  cdj3lem3 10365  cdj3lem3b 10367  ghomgrpilem2 10386  cayleylem2 10410  infi1 10447  infi1OLD 10448  cmpbva 10464  hmeogrp 10538  trnij 10637  stoi 10639  jdmo 10711

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain