Theorem eqtrd 1505

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 1484	. 2 |- (ph -> (A = B <-> A = C))
4	1, 3	mpbid 195	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  eqtr2d 1506  eqtr3d 1507  eqtr4d 1508  3eqtrd 1509  3eqtr2d 1511  3eqtr3d 1513  3eqtr4d 1515  syl5eq 1517  syl6eq 1521  sylan9eq 1525  csbidmg 2036  csbco3g 2037  uneq12d 2182  ineq12d 2215  opeq1 2484  opeq12d 2492  hbopd 2494  opprc1 2495  csbopabg 2674  opprc3 2793  moop2 2797  unisn3 2872  suceq 3030  ordunisuc 3085  orduniss2 3086  onuninsuc 3104  xpid11 3331  hbimad 3408  csbima12g 3409  coi2 3507  funcnvres2 3566  fnco 3591  fco 3631  foima 3671  f1imacnv 3700  f1ococnv2 3703  hbfvd 3725  hbfvd2 3726  csbfv12g 3737  csbfv2g 3738  csbfvg 3739  funfv2 3766  fopabco 3827  fopabcos 3828  fvresi 3838  funiunfv 3861  tfrlem11 3916  tz7.44-2 3924  rdglem2 3933  rdglim2 3944  abianfplem 3956  opreq12d 3973  hboprd 3977  csboprg 3981  csbopr12g 3982  csbopr1g 3983  csbopr2g 3984  curry1 4091  curry1val 4093  eloprabi 4111  oev 4146  oa0 4148  oev2 4155  oa1suc 4157  om1r 4170  oaass 4188  odi 4203  omass 4204  oelim2 4215  nnmsucr 4233  nneob 4248  ereq 4260  oprec 4311  ecoprass 4313  ecoprdi 4314  pw2en 4435  mapenlem1 4478  mapenlem2 4479  mapxpen 4484  xpmapenlem3 4487  unfilem3 4535  unifi 4541  fiint 4543  fodomfi 4549  opthreg 4587  r1val3 4662  rankxpsuc 4698  aceq5lem3 4720  aceq5lem4 4721  ac6lem 4737  kmlem9 4756  kmlem11 4758  kmlem12 4759  unidom 4791  unxpdomlem 4826  sucxpdom 4829  mulidpi 4997  addasspi 5006  mulasspi 5008  distrpi 5009  indpi 5017  mulidpq 5052  prlem934a 5120  prlem934b 5121  00sr 5191  recexsrlem 5195  mulresr 5240  ax0id 5264  ax1id 5265  axcnre 5269  addid2t 5312  add42t 5322  2addsubt 5372  pncant 5380  nppcant 5384  mulid2t 5400  muladd11t 5405  mul02t 5427  negdi2t 5439  subsubt 5445  nnncant 5449  mulm1t 5454  addsub4t 5456  pnpcant 5461  pnpcan2t 5462  recextlem1 5665  recid2t 5709  divrec2t 5713  dividt 5732  div0t 5733  divdivdivt 5751  recdivt 5756  lt2mul2divt 5832  nnmulclt 5899  times2t 5962  zltp1let 6138  nneo 6154  zneo 6157  zneoOLD 6158  uzindOLD 6166  uzrdgsuc 6254  seq1val 6262  seq1suclem 6266  ser1p1 6286  ser1add2 6288  ser1add 6289  shftval2t 6297  shftval4t 6299  shftval5t 6300  2shft 6302  shftcan2t 6303  iooval2t 6317  fzshftralt 6467  seqzfval 6482  seqzvalt 6485  seq1seq02t 6488  seqzp1 6493  seq0p1 6496  seqzval2t 6498  ser0p1 6512  expvalt 6515  expnnvalt 6517  exp1t 6518  expp1t 6519  recexpt 6540  expmult 6542  sqvalt 6554  subsqt 6587  subsq2t 6588  bernneq 6597  discrlem3 6603  sqrmsq2 6651  sqsqr 6666  replimt 6707  replimtOLD 6708  imret 6725  reim0bt 6727  resubt 6756  imsubt 6759  cjsubt 6766  cjexpt 6767  imcjt 6769  absnegt 6782  absvalsqt 6785  absvalsq2t 6786  sqabsaddt 6798  sqabssubt 6799  absreimsqt 6806  absexpt 6818  cjdiv 6841  abssuble0t 6849  abs1m 6856  recant 6857  ser1absdiflem 6881  faclbnd4lem4 6903  faclbnd6 6906  bcvalt 6910  bcn0t 6916  bcnp11t 6918  bcpasc 6922  sumeq12dv 6948  sumeq12rdv 6949  fsumserz 6952  fsum1p 6972  fsum2 6976  fsumcom 6981  fsumrev 6982  fsumrev2 6983  fsumshft 6984  fsumshftm 6985  fsummulc1 6986  fsum0 6992  fsumabs2mul 6997  ser1ser0 7001  serzrelem 7014  binomlem1 7019  binomlem2 7020  binomlem3 7021  binomlem4 7022  binom1p 7026  bcxmas 7029  climshft2 7059  climaddlem3 7069  climsub 7083  iserzex 7099  climsup 7108  ser1const 7124  ser10 7125  isumvalt 7145  fnsmntlem 7177  fnsmnt 7178  geoser 7186  geolimilem 7187  georeclim 7192  geosum 7193  cvgratlem1ALT 7199  cvgratlem1 7202  fsum0diaglem2 7209  fsum0diag2 7211  fsum0diag4 7213  negfcncf 7221  efcltlem2 7264  ef0lem 7269  erelem6 7283  efaddlem16 7312  efaddlem17 7313  efexpt 7331  eftabs 7334  ef1tllem 7340  ef01tllem2 7343  eirrlem2 7348  abspef01tlub 7353  absefm1le 7369  resinvalt 7392  recosvalt 7393  efi4pt 7394  resin4pt 7395  recos4pt 7396  sinnegt 7401  cosnegt 7402  efmivalt 7407  sinsubt 7414  cossubt 7415  addsint 7416  subsint 7417  subcost 7419  sincossqt 7420  sin2tt 7421  cos01bndlem3 7430  absefit 7441  abseft 7442  demoivre 7443  demoivreALT 7444  acdc3lem 7445  acdc3 7446  acdc2lem1 7447  acdc2lem2 7448  acdc2 7449  acdc5lem1 7450  acdc5lem2 7451  acdc5 7452  acdclem 7453  acdc 7454  ruclem4 7473  infxpidmlem2 7513  infxpidmlem3 7514  alephsuc3 7545  ntrval 7636  clsval 7637  ntrval2 7646  neival 7677  lpval 7703  cnfval 7716  cnpfval 7717  cnpval 7719  idcn 7726  cncnplem4 7737  ismet 7758  dfms2 7759  ismsg 7760  msflem 7763  metsym 7776  metreslem 7784  metxpdval 7791  metxpfval 7793  blfval 7797  blval 7799  blin 7814  cncfmet 7867  remetdval 7870  bl2ioo 7873  tgioolem 7876  lmconst 7896  lmfexlem2 7919  xpcn 7938  cncms 7960  bcthlem20 7980  isgrp 8003  grpidinvlem2 8011  grpidinv 8014  grpidval 8020  grpinvfval 8028  grpinvval 8029  grpdivfval 8043  grpdivval 8044  grpdivinv 8045  grpdivdiv 8049  grpdivid 8051  grpnpcan 8053  grpnnncan2 8055  grplactval 8060  abldivdiv 8072  ablnnncan 8075  ablnnncan1 8077  subgopr 8082  issubgi 8086  ablmul 8095  mulid 8096  isring 8105  ringi 8106  vci 8131  vcrinv 8155  vclinv 8156  vcsub4 8159  isvclem 8160  vcoprne 8162  vafval 8186  smfval 8188  0vfval 8189  invfval 8225  nvzs 8229  nvmdi 8234  nvrinv 8237  nvlinv 8238  nvpncan2 8240  nvaddsub4 8245  nvsge0 8255  nvm1 8256  nvabs 8265  nvop 8269  imsval 8280  imsdval 8281  imsdval2 8282  imsmetlem 8287  sqcn 8298  va1cnlem 8307  sm1cnilem 8309  ipfval 8314  ipval 8315  ipval2 8319  4ipval2 8320  ipval3 8321  4ipval3 8324  ipid 8325  ipcj 8329  ip0r 8332  sspmval 8354  sspival 8359  sspimsval 8361  lnoval 8375  lno0 8379  lnomul 8382  nmoval 8386  bloval 8401  0oval 8408  0lno 8410  nmo0 8411  blocnilem 8423  hmoval 8429  phop 8436  cnph 8437  ipasslem1 8449  ipasslem2 8450  ipasslem5 8453  ipasslem8 8456  ipdir 8461  ipdi 8462  ipass 8464  ipassr 8465  ipassr2 8466  ipsubdir 8467  ipsubdi 8468  sspph 8474  ubthlem8 8495  ubthlem9 8496  ubthlem10 8497  minveclem9 8512  minveclem18 8521  minveclem20 8523  minveclem23 8526  minveclem35 8538  htthlem5 8582  htthlem9 8586  isps 8603  spwval2 8610  spwval3 8611  spwnex3 8612  spwval 8616  sincolem 8619  sinmpi 8648  cosmpi 8649  efimpi 8650  sinq12gt0t 8660  efgh 8668  efghgrpilem 8669  efif 8671  circcltOLD 8691  circgrpOLD 8693  shftefif1olem 8696  efper 8702  relogexpt 8729  hvsubidt 8850  hv2negt 8852  hvaddsubvalt 8857  hvpncant 8863  hvsubdistr1t 8871  hvsub0t 8898  his52t 8909  his7t 8911  hiassdit 8912  his2subt 8913  his2sub2t 8914  hi01t 8917  hi02t 8918  abshicomt 8922  hilabl 8982  bcsALT 9001  hhcms 9027  norm1t 9076  hhssablt 9088  hhssnv 9089  hhssnvt 9090  hhsssh 9094  hhsscms 9105  pjthlem7 9180  pjthlem8 9181  pjvalt 9194  shscl 9236  chsupid 9266  chsupsn 9267  spanid 9272  chdmm2t 9404  chdmm3t 9405  chdmm4t 9406  chdmj2t 9408  chdmj3t 9409  chdmj4t 9410  elspansn2t 9446  spansneleq 9449  spansneleqOLD 9450  normcant 9456  pjspansnt 9457  fh1t 9518  fh2t 9519  osumlem2 9536  chsot 9546  pjsumt 9612  mayete3 9630  ho0valt 9633  hoaddass 9659  ho2co 9664  hoid1 9672  hoid1r 9673  homulid2t 9683  hosubdit 9691  hosub4t 9696  hosubsubt 9700  eigpos 9719  adjvalt 9771  adjval2t 9772  hmopadj2t 9822  bralnfnt 9829  nmopneg 9846  lnop0t 9847  lnopmult 9848  lnopaddmul 9854  lnopsubmul 9856  lnopmulsub 9857  homco2t 9858  lnopm 9881  lnophs 9882  lnopco 9884  lnopeq0 9888  nmopunt 9895  hmopst 9901  hmopmt 9902  nmbdoplb 9905  nmcoplb 9914  nmophm 9917  lnfnaddmul 9930  nmbdfnlb 9934  nmcfnlb 9943  nlelsh 9949  riesz3 9951  riesz4 9952  cnlnadjlem2 9957  adjaddt 9982  nmopcoadj 9990  branmfnt 9994  cnvbramult 10004  kbass5t 10009  leop2t 10013  leop3t 10014  leoprf2t 10016  leoprft 10017  idleop 10020  leopaddt 10021  leopmulit 10022  leopnmidt 10027  hmopidmcht 10037  hmopidmpjt 10038  pjadjco 10045  pjss1co 10047  pjss2co 10048  pjssum 10055  pjssdif2 10058  pjidmcot 10065  pjhmopidm 10066  dfpjopt 10067  elpjrnt 10073  pjclem4a 10082  pjclem4 10083  pjadj2co 10088  pj3lem1 10090  pj3s 10091  hstpytht 10112  hstoht 10115  st0 10132  strlem1 10133  strlem3a 10135  hstrlem3a 10143  golem1 10154  stcltrlem1 10159  dmdmdt 10183  dmdbr5 10191  dmdsl3t 10198  mdsl3t 10199  mdslmd3 10215  irredlem2 10274  atabs 10284  sumdmdlem2 10302  cdj3lem2 10318  ghomgrpilem2 10342  ghomgrplem 10345  ghomfo 10347  ghomid 10350  elgiso 10354  symggrpi 10362  cayleylem2 10366  cayleylem3 10367  11st22nd 10412  idhme 10468  hmeogrp 10484  sfvlim 10522  mslb1 10545  msra3 10547  iint 10550  cnvtr 10554  domval 10571  codval 10572  idval 10573  cmpval 10574  eloi 10575  iscat 10603  cati 10604  ishomb 10632  cmpassoh 10645  homgrf 10646  isfuna 10664  idfisf 10670

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

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

Copyright terms: Public domain