Theorem eqtrd 1544

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
eqtrd.1	|- (ph -> A = B)
eqtrd.2	|- (ph -> B = C)

Assertion

Ref	Expression
eqtrd	|- (ph -> A = C)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 |- (ph -> A = B)
2		eqtrd.2	. . 3 |- (ph -> B = C)
3	2	eqeq2d 1523	. 2 |- (ph -> (A = B <-> A = C))
4	1, 3	mpbid 193	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 988

This theorem is referenced by:  eqtr2d 1545  eqtr3d 1546  eqtr4d 1547  3eqtrd 1548  3eqtr2d 1550  3eqtr3d 1552  3eqtr4d 1554  syl5eq 1556  syl6eq 1560  sylan9eq 1564  csbidmg 2083  csbco3g 2084  uneq12d 2229  ineq12d 2262  opeq1 2535  opeq12d 2543  hbopd 2545  opprc1 2546  csbopabg 2729  opprc3 2850  moop2 2854  unisn3 2930  suceq 3089  ordunisuc 3144  orduniss2 3145  onuninsuci 3163  xpid11 3395  hbimad 3475  csbima12g 3476  coi2 3585  funcnvres2 3645  fnco 3670  fco 3711  foima 3752  f1imacnv 3781  f1ococnv2 3784  hbfvd 3806  hbfvd2 3807  csbfv12g 3818  csbfv2g 3819  csbfvg 3820  funfv2 3847  fopabco 3908  fopabcos 3909  fvresi 3919  funiunfv 3942  tfrlem11 3997  tz7.44-2 4005  rdglem2 4014  rdglim2 4025  abianfplem 4037  opreq12d 4054  hboprd 4058  csboprg 4062  csbopr12g 4063  csbopr1g 4064  csbopr2g 4065  eloprabi 4198  curry1 4208  curry1val 4210  curry2 4211  oev 4237  oa0 4239  oev2 4246  oa1suc 4248  om1r 4261  oaass 4279  odi 4294  omass 4295  oelim2 4306  nnmsucr 4324  nneob 4339  ereq 4351  oprec 4405  ecoprass 4407  ecoprdi 4408  pw2en 4533  mapenlem1 4578  mapenlem2 4579  mapxpen 4584  xpmapenlem3 4587  unfilem3 4637  unifi 4642  fiint 4644  fodomfi 4650  opthreg 4690  r1val3 4765  rankxpsuc 4801  aceq5lem3 4823  aceq5lem4 4824  ac6lem 4840  kmlem9 4859  kmlem11 4861  kmlem12 4862  unidom 4894  unxpdomlem 4932  sucxpdom 4935  mulidpi 5103  addasspi 5112  mulasspi 5114  distrpi 5115  indpi 5123  mulidpq 5158  prlem934a 5226  prlem934b 5227  00sr 5297  recexsrlem 5301  mulresr 5346  ax0id 5370  ax1id 5371  axcnre 5375  addid2 5418  add42 5428  2addsub 5478  pncan 5486  nppcan 5490  mulid2 5506  muladd11 5511  mul02 5533  negdi2 5545  subsub 5551  nnncan 5555  mulm1 5560  addsub4 5562  pnpcan 5567  pnpcan2 5568  recextlem1 5771  divcan2 5810  recid2 5819  divrec2 5823  divcan4 5842  divid 5845  div0 5846  divdivdiv 5867  divdivdivOLD 5868  recdiv 5873  lt2mul2divOLD 5958  nnmulcl 6028  times2 6093  zltp1le 6291  nneoi 6310  zneo 6313  uzindOLD 6321  quoremz 6391  quoremnn0 6393  fldiv 6396  fldiv2 6397  modfrac 6404  modid 6409  modcyc 6410  modcycOLD 6411  modcyc2 6412  modcyc2OLD 6413  iooval2 6426  ioojoin 6476  fzshftral 6582  uzrdgsuci 6597  seq1val 6605  seq1suclem 6609  ser1p1i 6629  ser1add2i 6631  ser1addi 6632  shftval2 6640  shftval4 6642  shftval5 6643  2shfti 6645  shftcan2 6646  seqzfval 6660  seqzval 6663  seq1seq02 6666  seqzp1 6671  seq0p1 6674  seqzval2 6676  ser0p1i 6690  expval 6693  expnnval 6695  exp1 6696  expp1 6697  recexpOLD 6718  expmul 6720  sqval 6731  subsq 6764  subsq2 6765  bernneq 6774  discrlem3 6781  sqrmsq2i 6829  sqsqri 6844  replim 6884  imre 6896  reim0b 6898  resub 6929  imsub 6932  cjsub 6939  cjexp 6940  imcj 6942  absneg 6955  absvalsq 6958  absvalsq2 6959  sqabsadd 6971  sqabssub 6972  absreimsq 6979  absexp 6991  cjdivi 7011  abssuble0 7019  absmax 7020  abs1mi 7027  recan 7028  ser1absdiflem 7052  faclbnd4lem4 7074  faclbnd6 7077  bcval 7081  bcn0 7086  bcnp11 7088  bcpasci 7092  sumeq12dv 7118  sumeq12rdv 7119  fsumserz 7122  fsum1p 7142  fsum2 7146  fsumcom 7151  fsumrev 7152  fsumrev2 7153  fsumshft 7154  fsumshftm 7155  fsummulc1 7156  fsum0 7162  fsumabs2mul 7167  ser1ser0i 7171  serzrelem 7184  binomlem1 7189  binomlem2 7190  binomlem3 7191  binomlem4 7192  binom1pi 7196  bcxmas 7199  climshft2i 7229  climaddlem3 7239  climsub 7253  iserzexi 7269  climsupi 7278  caucvg3ai 7287  caucvg3lem 7289  ser1consti 7294  ser10 7295  isumval 7315  arisumilem 7348  arisumi 7349  geoseri 7357  geolimilem 7358  georeclim 7363  geosumi 7364  cvgratlem1ALT 7370  cvgratlem1 7373  fsum0diaglem2 7380  fsum0diag2 7382  fsum0diag4 7384  negfcncfi 7392  efcltlem2 7428  ef0lem 7433  erelem6 7447  efaddlem16 7476  efaddlem17 7477  efexp 7495  eftabsi 7498  ef1tllem 7504  ef01tllem2 7507  ef01tllem2OLD 7508  eirrlem2 7513  abspef01tlubi 7519  absefm1lei 7536  resinval 7557  recosval 7558  efi4p 7559  resin4p 7560  recos4p 7561  sinneg 7566  cosneg 7567  efmival 7572  sinsub 7579  cossub 7580  addsin 7581  subsin 7582  subcos 7584  sincossq 7585  sin2t 7586  cos01bndlem3 7596  absefi 7607  absef 7608  demoivre 7609  demoivreALT 7610  acdc3lem 7611  acdc3 7612  acdc2lem1 7613  acdc2lem2 7614  acdc2 7615  acdc5lem1 7616  acdc5lem2 7617  acdc5 7618  acdclem 7619  acdc 7620  ruclem4 7638  infxpidmlem2 7678  infxpidmlem3 7679  alephsuc3 7710  ntrval 7796  clsval 7797  ntrval2 7806  neival 7837  lpval 7863  cnfval 7876  cnpfval 7877  cnpval 7879  idcn 7886  cncnplem4 7897  ismet 7918  dfms2 7919  ismsg 7920  msflem 7923  metsym 7936  metreslem 7942  metxpdval 7949  metxpfval 7951  blfval 7955  blval 7957  blin 7972  cncfmet 8025  remetdval 8028  bl2ioo 8031  tgioolem 8034  lmconst 8054  lmfexlem2 8077  xpcn 8096  cncms 8118  bcthlem20 8138  isgrp 8161  grpidinvlem2 8169  grpidinv 8172  grpidval 8177  grpinvfval 8185  grpinvval 8186  grpdivfval 8200  grpdivval 8201  grpdivinv 8202  grpdivdiv 8206  grpdivid 8208  grpnpcan 8210  grpnnncan2 8212  grplactval 8216  abldivdiv 8227  ablnnncan 8230  ablnnncan1 8232  subgopr 8237  issubgi 8241  ablmul 8250  mulid 8251  isring 8260  ringi 8261  vci 8286  vcrinv 8310  vclinv 8311  vcsub4 8314  isvclem 8315  vcoprne 8317  vafval 8341  smfval 8343  0vfval 8344  invfval 8380  nvzs 8384  nvmdi 8389  nvrinv 8392  nvlinv 8393  nvpncan2 8395  nvaddsub4 8400  nvsge0 8410  nvm1 8411  nvabs 8420  nvop 8424  imsval 8435  imsdval 8436  imsdval2 8437  imsmetlem 8442  sqcn 8454  va1cnlem 8464  sm1cnilem 8466  ipfval 8471  ipval 8472  ipval2 8476  4ipval2 8477  ipval3 8478  4ipval3 8481  ipid 8482  ipcj 8486  ip0r 8489  sspmval 8511  sspival 8516  sspimsval 8518  lnoval 8532  lno0 8536  lnomul 8540  nmoval 8545  bloval 8560  0oval 8567  0lno 8569  nmo0 8570  blocnilem 8583  hmoval 8589  phop 8596  cnph 8597  ipasslem1 8609  ipasslem2 8610  ipasslem5 8613  ipasslem8 8616  ipdir 8621  ipdi 8622  ipass 8624  ipassr 8625  ipassr2 8626  ipsubdir 8627  ipsubdi 8628  sspph 8634  ubthlem8 8655  ubthlem9 8656  ubthlem10 8657  minveclem9 8672  minveclem18 8681  minveclem20 8683  minveclem23 8686  minveclem35 8698  htthlem5 8743  htthlem9 8747  isps 8764  spwval2 8772  spwval3 8773  spwnex3 8774  spwval 8778  sincolem 8783  sinmpi 8812  cosmpi 8813  sinppi 8814  cosppi 8815  sinkpi 8816  efimpi 8817  sinq12gt0t 8827  abssinper 8831  sineq0 8832  efgh 8837  efghgrpilem 8838  efif 8840  shftefif1olem 8860  efper 8866  relogexp 8893  hvsubid 9014  hv2neg 9016  hvaddsubval 9021  hvpncan 9027  hvsubdistr1 9035  hvsub0 9063  his52 9074  his7 9076  hiassdi 9077  his2sub 9078  his2sub2 9079  hi01 9082  hi02 9083  abshicom 9087  hilabl 9147  bcsiALT 9166  hhcms 9192  norm1 9241  hhssabl 9253  hhssnv 9254  hhssnvt 9255  hhsssh 9259  hhsscms 9270  pjthlem7 9345  pjthlem8 9346  pjval 9359  shscli 9401  chsupid 9431  chsupsn 9432  spanid 9437  chdmm2 9569  chdmm3 9570  chdmm4 9571  chdmj2 9573  chdmj3 9574  chdmj4 9575  elspansn2 9610  spansneleq 9613  normcan 9619  pjspansn 9620  fh1 9681  fh2 9682  osumlem2 9699  chso 9709  pjsumi 9775  mayete3i 9793  ho0val 9796  hoaddassi 9822  ho2coi 9827  hoid1i 9835  hoid1ri 9836  homulid2 9846  hosubdi 9854  hosub4 9859  hosubsub 9863  eigposi 9882  adjval 9932  adjval2 9933  hmopadj2 9983  bralnfn 9990  nmopnegi 10006  lnop0 10007  lnopmul 10008  lnopaddmuli 10014  lnopsubmuli 10016  lnopmulsubi 10017  homco2 10018  lnopmi 10042  lnophsi 10043  lnopcoi 10045  lnopeq0i 10049  nmopun 10056  hmops 10062  hmopm 10063  nmbdoplbi 10066  nmcoplbi 10075  nmophmi 10078  lnfnaddmuli 10091  nmbdfnlbi 10095  nmcfnlbi 10104  nlelshi 10110  riesz3i 10112  riesz4i 10113  cnlnadjlem2 10118  adjadd 10143  nmopcoadji 10151  branmfn 10155  cnvbramul 10165  kbass5 10170  leop2 10174  leop3 10175  leoprf2 10177  leoprf 10178  idleop 10181  leopadd 10182  leopmuli 10183  leopnmid 10188  hmopidmch 10198  hmopidmpj 10199  pjadjcoi 10206  pjss1coi 10208  pjss2coi 10209  pjssumi 10216  pjssdif2i 10219  pjidmco 10226  pjhmopidm 10227  dfpjop 10228  elpjrn 10235  pjclem4a 10244  pjclem4 10245  pjadj2coi 10250  pj3lem1 10252  pj3si 10253  hstpyth 10274  hstoh 10277  st0 10294  strlem1 10295  strlem3a 10297  hstrlem3a 10305  golem1 10316  stcltrlem1 10321  dmdmd 10345  dmdbr5 10353  dmdsl3 10360  mdsl3 10361  mdslmd3i 10377  irredlem2 10436  atabsi 10446  sumdmdlem2 10464  cdj3lem2 10480  ghomgrpilem2 10507  ghomgrplem 10510  ghomfo 10512  ghomid 10515  elgiso 10519  symggrpi 10527  cayleylem2 10531  cayleylem3 10532  11st22nd 10576  fveq12d 10607  vri 10625  idhme 10658  hmeogrp 10674  sfvlim 10729  sfvlimOLD 10730  mslb1 10765  msra3 10767  iint 10770  cnvtr 10774  domval 10790  codval 10791  idval 10792  cmpval 10793  eloi 10794  iscat 10822  cati 10823  ishomb 10851  cmpassoh 10864  homgrf 10865  isepia 10882  cinvlem1 10890  idfisf 10902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain