Theorem eqtrd 1507

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  eqtr2d 1508  eqtr3d 1509  eqtr4d 1510  3eqtrd 1511  3eqtr2d 1513  3eqtr3d 1515  3eqtr4d 1517  syl5eq 1519  syl6eq 1523  sylan9eq 1527  csbidmg 2039  csbco3g 2040  uneq12d 2185  ineq12d 2218  opeq1 2487  opeq12d 2495  hbopd 2497  opprc1 2498  csbopabg 2678  opprc3 2797  moop2 2801  unisn3 2876  suceq 3034  ordunisuc 3089  orduniss2 3090  onuninsuc 3108  xpid11 3335  hbimad 3412  csbima12g 3413  coi2 3511  funcnvres2 3570  fnco 3595  fco 3636  foima 3676  f1imacnv 3705  f1ococnv2 3708  hbfvd 3730  hbfvd2 3731  csbfv12g 3742  csbfv2g 3743  csbfvg 3744  funfv2 3771  fopabco 3832  fopabcos 3833  fvresi 3843  funiunfv 3866  tfrlem11 3921  tz7.44-2 3929  rdglem2 3938  rdglim2 3949  abianfplem 3961  opreq12d 3978  hboprd 3982  csboprg 3986  csbopr12g 3987  csbopr1g 3988  csbopr2g 3989  curry1 4098  curry1val 4100  eloprabi 4118  oev 4153  oa0 4155  oev2 4162  oa1suc 4164  om1r 4177  oaass 4195  odi 4210  omass 4211  oelim2 4222  nnmsucr 4240  nneob 4255  ereq 4267  oprec 4318  ecoprass 4320  ecoprdi 4321  pw2en 4444  mapenlem1 4487  mapenlem2 4488  mapxpen 4493  xpmapenlem3 4496  unfilem3 4545  unifi 4550  fiint 4552  fodomfi 4558  opthreg 4596  r1val3 4671  rankxpsuc 4707  aceq5lem3 4729  aceq5lem4 4730  ac6lem 4746  kmlem9 4765  kmlem11 4767  kmlem12 4768  unidom 4800  unxpdomlem 4835  sucxpdom 4838  mulidpi 5006  addasspi 5015  mulasspi 5017  distrpi 5018  indpi 5026  mulidpq 5061  prlem934a 5129  prlem934b 5130  00sr 5200  recexsrlem 5204  mulresr 5249  ax0id 5273  ax1id 5274  axcnre 5278  addid2t 5321  add42t 5331  2addsubt 5381  pncant 5389  nppcant 5393  mulid2t 5409  muladd11t 5414  mul02t 5436  negdi2t 5448  subsubt 5454  nnncant 5458  mulm1t 5463  addsub4t 5465  pnpcant 5470  pnpcan2t 5471  recextlem1 5673  divcan2t 5714  recid2t 5724  divrec2t 5728  divcan4t 5750  dividt 5754  div0t 5755  divdivdivt 5773  recdivt 5778  lt2mul2divt 5860  nnmulclt 5929  times2t 5993  zltp1let 6169  nneo 6185  zneo 6188  uzindOLD 6196  quoremOLD 6238  uzrdgsuc 6290  seq1val 6298  seq1suclem 6302  ser1p1 6322  ser1add2 6324  ser1add 6325  shftval2t 6333  shftval4t 6335  shftval5t 6336  2shft 6338  shftcan2t 6339  iooval2t 6353  ioojoint 6402  fzshftralt 6508  seqzfval 6523  seqzvalt 6526  seq1seq02t 6529  seqzp1 6534  seq0p1 6537  seqzval2t 6539  ser0p1 6553  expvalt 6556  expnnvalt 6558  exp1t 6559  expp1t 6560  recexpt 6581  expmult 6583  sqvalt 6595  subsqt 6628  subsq2t 6629  bernneq 6638  discrlem3 6644  sqrmsq2 6692  sqsqr 6707  replimt 6747  imret 6759  reim0bt 6761  resubt 6791  imsubt 6794  cjsubt 6801  cjexpt 6802  imcjt 6804  absnegt 6817  absvalsqt 6820  absvalsq2t 6821  sqabsaddt 6833  sqabssubt 6834  absreimsqt 6841  absexpt 6853  cjdiv 6873  abssuble0t 6881  absmaxt 6882  abs1m 6889  recant 6890  ser1absdiflem 6914  faclbnd4lem4 6936  faclbnd6 6939  bcvalt 6943  bcn0t 6948  bcnp11t 6950  bcpasc 6954  sumeq12dv 6980  sumeq12rdv 6981  fsumserz 6984  fsum1p 7004  fsum2 7008  fsumcom 7013  fsumrev 7014  fsumrev2 7015  fsumshft 7016  fsumshftm 7017  fsummulc1 7018  fsum0 7024  fsumabs2mul 7029  ser1ser0 7033  serzrelem 7046  binomlem1 7051  binomlem2 7052  binomlem3 7053  binomlem4 7054  binom1p 7058  bcxmas 7061  climshft2 7091  climaddlem3 7101  climsub 7115  iserzex 7131  climsup 7140  caucvg3a 7149  caucvg3lem 7151  ser1const 7156  ser10 7157  isumvalt 7177  fnsmntlem 7210  fnsmnt 7211  geoser 7219  geolimilem 7220  georeclim 7225  geosum 7226  cvgratlem1ALT 7232  cvgratlem1 7235  fsum0diaglem2 7242  fsum0diag2 7244  fsum0diag4 7246  negfcncf 7254  efcltlem2 7290  ef0lem 7295  erelem6 7309  efaddlem16 7338  efaddlem17 7339  efexpt 7357  eftabs 7360  ef1tllem 7366  ef01tllem2 7369  ef01tllem2OLD 7370  eirrlem2 7375  abspef01tlub 7380  absefm1le 7397  resinvalt 7418  recosvalt 7419  efi4pt 7420  resin4pt 7421  recos4pt 7422  sinnegt 7427  cosnegt 7428  efmivalt 7433  sinsubt 7440  cossubt 7441  addsint 7442  subsint 7443  subcost 7445  sincossqt 7446  sin2tt 7447  cos01bndlem3 7456  absefit 7467  abseft 7468  demoivre 7469  demoivreALT 7470  acdc3lem 7471  acdc3 7472  acdc2lem1 7473  acdc2lem2 7474  acdc2 7475  acdc5lem1 7476  acdc5lem2 7477  acdc5 7478  acdclem 7479  acdc 7480  ruclem4 7498  infxpidmlem2 7538  infxpidmlem3 7539  alephsuc3 7570  ntrval 7661  clsval 7662  ntrval2 7671  neival 7702  lpval 7728  cnfval 7741  cnpfval 7742  cnpval 7744  idcn 7751  cncnplem4 7762  ismet 7783  dfms2 7784  ismsg 7785  msflem 7788  metsym 7801  metreslem 7807  metxpdval 7814  metxpfval 7816  blfval 7820  blval 7822  blin 7837  cncfmet 7890  remetdval 7893  bl2ioo 7896  tgioolem 7899  lmconst 7919  lmfexlem2 7942  xpcn 7961  cncms 7983  bcthlem20 8003  isgrp 8026  grpidinvlem2 8034  grpidinv 8037  grpidval 8043  grpinvfval 8051  grpinvval 8052  grpdivfval 8066  grpdivval 8067  grpdivinv 8068  grpdivdiv 8072  grpdivid 8074  grpnpcan 8076  grpnnncan2 8078  grplactval 8082  abldivdiv 8093  ablnnncan 8096  ablnnncan1 8098  subgopr 8103  issubgi 8107  ablmul 8116  mulid 8117  isring 8126  ringi 8127  vci 8152  vcrinv 8176  vclinv 8177  vcsub4 8180  isvclem 8181  vcoprne 8183  vafval 8207  smfval 8209  0vfval 8210  invfval 8246  nvzs 8250  nvmdi 8255  nvrinv 8258  nvlinv 8259  nvpncan2 8261  nvaddsub4 8266  nvsge0 8276  nvm1 8277  nvabs 8286  nvop 8290  imsval 8301  imsdval 8302  imsdval2 8303  imsmetlem 8308  sqcn 8320  va1cnlem 8330  sm1cnilem 8332  ipfval 8337  ipval 8338  ipval2 8342  4ipval2 8343  ipval3 8344  4ipval3 8347  ipid 8348  ipcj 8352  ip0r 8355  sspmval 8377  sspival 8382  sspimsval 8384  lnoval 8398  lno0 8402  lnomul 8406  nmoval 8411  bloval 8426  0oval 8433  0lno 8435  nmo0 8436  blocnilem 8449  hmoval 8455  phop 8462  cnph 8463  ipasslem1 8475  ipasslem2 8476  ipasslem5 8479  ipasslem8 8482  ipdir 8487  ipdi 8488  ipass 8490  ipassr 8491  ipassr2 8492  ipsubdir 8493  ipsubdi 8494  sspph 8500  ubthlem8 8521  ubthlem9 8522  ubthlem10 8523  minveclem9 8538  minveclem18 8547  minveclem20 8549  minveclem23 8552  minveclem35 8564  htthlem5 8609  htthlem9 8613  isps 8630  spwval2 8638  spwval3 8639  spwnex3 8640  spwval 8644  sincolem 8650  sinmpi 8679  cosmpi 8680  sinppi 8681  sinkpi 8682  efimpi 8683  sinq12gt0t 8693  abssinper 8697  sineq0 8698  efgh 8703  efghgrpilem 8704  efif 8706  shftefif1olem 8726  efper 8732  relogexpt 8759  hvsubidt 8880  hv2negt 8882  hvaddsubvalt 8887  hvpncant 8893  hvsubdistr1t 8901  hvsub0t 8928  his52t 8939  his7t 8941  hiassdit 8942  his2subt 8943  his2sub2t 8944  hi01t 8947  hi02t 8948  abshicomt 8952  hilabl 9012  bcsALT 9031  hhcms 9057  norm1t 9106  hhssablt 9118  hhssnv 9119  hhssnvt 9120  hhsssh 9124  hhsscms 9135  pjthlem7 9210  pjthlem8 9211  pjvalt 9224  shscl 9266  chsupid 9296  chsupsn 9297  spanid 9302  chdmm2t 9434  chdmm3t 9435  chdmm4t 9436  chdmj2t 9438  chdmj3t 9439  chdmj4t 9440  elspansn2t 9475  spansneleq 9478  normcant 9484  pjspansnt 9485  fh1t 9546  fh2t 9547  osumlem2 9564  chsot 9574  pjsumt 9640  mayete3 9658  ho0valt 9661  hoaddass 9687  ho2co 9692  hoid1 9700  hoid1r 9701  homulid2t 9711  hosubdit 9719  hosub4t 9724  hosubsubt 9728  eigpos 9747  adjvalt 9799  adjval2t 9800  hmopadj2t 9850  bralnfnt 9857  nmopneg 9874  lnop0t 9875  lnopmult 9876  lnopaddmul 9882  lnopsubmul 9884  lnopmulsub 9885  homco2t 9886  lnopm 9910  lnophs 9911  lnopco 9913  lnopeq0 9917  nmopunt 9924  hmopst 9930  hmopmt 9931  nmbdoplb 9934  nmcoplb 9943  nmophm 9946  lnfnaddmul 9959  nmbdfnlb 9963  nmcfnlb 9972  nlelsh 9978  riesz3 9980  riesz4 9981  cnlnadjlem2 9986  adjaddt 10011  nmopcoadj 10019  branmfnt 10023  cnvbramult 10033  kbass5t 10038  leop2t 10042  leop3t 10043  leoprf2t 10045  leoprft 10046  idleop 10049  leopaddt 10050  leopmulit 10051  leopnmidt 10056  hmopidmcht 10066  hmopidmpjt 10067  pjadjco 10074  pjss1co 10076  pjss2co 10077  pjssum 10084  pjssdif2 10087  pjidmcot 10094  pjhmopidm 10095  dfpjopt 10096  elpjrnt 10102  pjclem4a 10111  pjclem4 10112  pjadj2co 10117  pj3lem1 10119  pj3s 10120  hstpytht 10141  hstoht 10144  st0 10161  strlem1 10162  strlem3a 10164  hstrlem3a 10172  golem1 10183  stcltrlem1 10188  dmdmdt 10212  dmdbr5 10220  dmdsl3t 10227  mdsl3t 10228  mdslmd3 10244  irredlem2 10303  atabs 10313  sumdmdlem2 10331  cdj3lem2 10347  ghomgrpilem2 10371  ghomgrplem 10374  ghomfo 10376  ghomid 10379  elgiso 10383  symggrpi 10391  cayleylem2 10395  cayleylem3 10396  11st22nd 10437  idhme 10494  hmeogrp 10510  sfvlim 10549  mslb1 10572  msra3 10574  iint 10577  cnvtr 10581  domval 10598  codval 10599  idval 10600  cmpval 10601  eloi 10602  iscat 10630  cati 10631  ishomb 10659  cmpassoh 10672  homgrf 10673  isfuna 10691  idfisf 10697

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