Theorem eqtrd 1499

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

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  eqtr2d 1500  eqtr3d 1501  eqtr4d 1502  3eqtrd 1503  3eqtr2d 1505  3eqtr3d 1507  3eqtr4d 1509  syl5eq 1511  syl6eq 1515  sylan9eq 1519  csbidmg 2029  csbco3g 2030  uneq12d 2175  ineq12d 2208  opeq1 2478  opeq12d 2486  hbopd 2488  opprc1 2489  csbopabg 2668  opprc3 2787  moop2 2790  suceq 3024  ordunisuc 3079  orduniss2 3080  onuninsuc 3098  xpid11 3324  hbimad 3396  csbima12g 3397  coi2 3497  funcnvres2 3556  fnco 3581  fco 3621  foima 3661  f1imacnv 3690  f1ococnv2 3693  hbfvd 3715  hbfvd2 3716  csbfv12g 3727  csbfv2g 3728  csbfvg 3729  funfv2 3756  fopabco 3817  fopabcos 3818  fvresi 3828  funiunfv 3851  tfrlem11 3906  tz7.44-2 3914  rdglem2 3923  rdglim2 3934  abianfplem 3946  opreq12d 3963  hboprd 3967  csboprg 3971  csbopr12g 3972  csbopr1g 3973  csbopr2g 3974  curry1 4082  curry1val 4084  eloprabi 4102  oev 4137  oa0 4139  oev2 4146  oa1suc 4148  om1r 4161  oaass 4179  odi 4194  omass 4195  oelim2 4206  nnmsucr 4224  nneob 4239  ereq 4251  oprec 4302  ecoprass 4304  ecoprdi 4305  pw2en 4426  mapenlem1 4469  mapenlem2 4470  mapxpen 4475  xpmapenlem3 4478  unfilem3 4526  unifi 4532  fiint 4534  fodomfi 4540  opthreg 4576  r1val3 4651  rankxpsuc 4687  aceq5lem3 4709  aceq5lem4 4710  ac6lem 4726  kmlem9 4745  kmlem11 4747  kmlem12 4748  unidom 4780  unxpdomlem 4815  sucxpdom 4818  mulidpi 4986  addasspi 4995  mulasspi 4997  distrpi 4998  indpi 5006  mulidpq 5041  prlem934a 5109  prlem934b 5110  00sr 5180  recexsrlem 5184  mulresr 5229  ax0id 5253  ax1id 5254  axcnre 5258  addid2t 5301  add42t 5311  2addsubt 5361  pncant 5369  nppcant 5373  mulid2t 5389  muladd11t 5394  mul02t 5416  negdi2t 5428  subsubt 5434  nnncant 5438  mulm1t 5443  addsub4t 5445  pnpcant 5450  pnpcan2t 5451  recextlem1 5655  recid2t 5699  divrec2t 5703  dividt 5722  div0t 5723  divdivdivt 5741  recdivt 5746  lt2mul2divt 5822  nnmulclt 5889  times2t 5952  zltp1let 6128  nneo 6144  zneo 6147  zneoOLD 6148  uzindOLD 6156  uzrdgsuc 6241  seq1val 6249  seq1suclem 6253  ser1p1 6273  ser1add2 6275  ser1add 6276  shftval2t 6284  shftval4t 6286  shftval5t 6287  2shft 6289  shftcan2t 6290  iooval2t 6304  fzshftralt 6454  seqzfval 6469  seqzvalt 6472  seq1seq02t 6475  seqzp1 6480  seq0p1 6483  seqzval2t 6485  ser0p1 6499  expvalt 6502  expnnvalt 6504  exp1t 6505  expp1t 6506  recexpt 6526  expmult 6528  sqvalt 6540  subsqt 6573  subsq2t 6574  bernneq 6583  discrlem3 6588  sqrmsq2 6636  sqsqr 6651  replimt 6692  replimtOLD 6693  imret 6710  reim0bt 6712  resubt 6741  imsubt 6744  cjsubt 6751  cjexpt 6752  imcjt 6754  absnegt 6767  absvalsqt 6770  absvalsq2t 6771  sqabsaddt 6783  sqabssubt 6784  absreimsqt 6791  absexpt 6803  cjdiv 6826  abssuble0t 6834  abs1m 6841  recant 6842  ser1absdiflem 6866  faclbnd4lem4 6888  faclbnd6 6891  bcvalt 6895  bcn0t 6901  bcnp11t 6903  bcpasc 6907  sumeq12dv 6933  sumeq12rdv 6934  fsumserz 6937  fsum1p 6957  fsum2 6961  fsumcom 6966  fsumrev 6967  fsumrev2 6968  fsumshft 6969  fsumshftm 6970  fsummulc1 6971  fsum0 6977  fsumabs2mul 6982  ser1ser0 6986  serzrelem 6999  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binom1p 7011  bcxmas 7014  climshft2 7043  climaddlem3 7052  climsub 7066  iserzex 7082  climsup 7091  ser1const 7107  ser10 7108  isumvalt 7128  fnsmntlem 7160  fnsmnt 7161  geoser 7169  geolimilem 7170  georeclim 7175  geosum 7176  cvgratlem1ALT 7182  cvgratlem1 7185  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag4 7196  negfcncf 7204  efcltlem2 7247  ef0lem 7252  erelem6 7266  efaddlem16 7295  efaddlem17 7296  efexpt 7314  eftabs 7317  ef1tllem 7323  ef01tllem2 7326  eirrlem2 7331  abspef01tlub 7336  absefm1le 7352  resinvalt 7375  recosvalt 7376  efi4pt 7377  resin4pt 7378  recos4pt 7379  sinnegt 7384  cosnegt 7385  efmivalt 7390  sinsubt 7397  cossubt 7398  addsint 7399  subsint 7400  subcost 7402  sincossqt 7403  sin2tt 7404  cos01bndlem3 7413  absefit 7424  abseft 7425  demoivre 7426  demoivreALT 7427  acdc3lem 7428  acdc3 7429  acdc2lem1 7430  acdc2lem2 7431  acdc2 7432  acdc5lem1 7433  acdc5lem2 7434  acdc5 7435  acdclem 7436  acdc 7437  ruclem4 7456  infxpidmlem2 7496  infxpidmlem3 7497  alephsuc3 7527  ntrval 7618  clsval 7619  ntrval2 7628  neival 7658  lpval 7684  cnfval 7696  cnpfval 7697  cnpval 7699  idcn 7705  cncnplem4 7716  ismet 7737  dfms2 7738  ismsg 7739  msflem 7742  metsym 7755  metreslem 7762  metxpdval 7769  metxpfval 7771  blfval 7775  blval 7777  blin 7792  cncfmet 7844  remetdval 7847  bl2ioo 7850  tgioolem 7853  lmconst 7872  lmfexlem2 7892  xpcn 7910  cncms 7932  bcthlem20 7952  isgrp 7975  grpidinvlem2 7983  grpidinv 7986  grpidval 7992  grpinvfval 8000  grpinvval 8001  grpdivfval 8016  grpdivval 8017  grpdivinv 8018  grpdivdiv 8022  grpdivid 8024  grpnpcan 8026  grpnnncan2 8028  grplactval 8033  abldivdiv 8045  ablnnncan 8048  ablnnncan1 8050  subgopr 8055  issubgi 8059  ablmul 8068  mulid 8069  isring 8078  ringi 8079  vci 8104  vcrinv 8128  vclinv 8129  vcsub4 8132  isvcgOLD 8133  isvclem 8134  vcoprne 8136  vafval 8160  smfval 8162  0vfval 8163  invfval 8201  nvzs 8205  nvmdi 8210  nvrinv 8213  nvlinv 8214  nvpncan2 8216  nvaddsub4 8221  nvsge0 8230  nvm1 8231  nvabs 8240  nvop 8244  imsval 8254  imsdval 8255  imsdval2 8256  imsmetlem 8261  sqcn 8270  va1cnlem 8279  sm1cnilem 8281  ipfval 8286  ipval 8287  ipval2 8291  4ipval2 8292  ipval3 8293  4ipval3 8296  ipid 8297  ipcj 8301  ip0r 8304  sspmval 8326  sspival 8331  sspimsval 8333  lnoval 8347  lno0 8351  lnomul 8354  nmoval 8358  bloval 8373  0oval 8380  0lno 8382  nmo0 8383  blocnilem 8395  hmoval 8401  phop 8408  cnph 8409  ipasslem1 8421  ipasslem2 8422  ipasslem5 8425  ipasslem8 8428  ipdir 8433  ipdi 8434  ipass 8436  ipassr 8437  ipassr2 8438  ipsubdir 8439  ipsubdi 8440  sspph 8446  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  minveclem9 8484  minveclem18 8493  minveclem20 8495  minveclem23 8498  minveclem35 8510  htthlem5 8554  htthlem9 8558  isps 8571  spwval2 8577  spwval3 8578  spwnex3 8579  spwval 8582  sincolem 8584  sinmpi 8613  cosmpi 8614  efimpi 8615  sinq12gt0t 8625  efgh 8633  efghgrpilem 8634  efif 8636  circcltOLD 8656  circgrpOLD 8658  shftefif1olem 8661  shftefif1olemOLD 8662  efper 8669  relogexpt 8696  logeftOLD 8705  logexptOLD 8712  hvsubidt 8816  hv2negt 8818  hvaddsubvalt 8823  hvpncant 8829  hvsubdistr1t 8837  hvsub0t 8864  his52t 8875  his7t 8877  hiassdit 8878  his2subt 8879  his2sub2t 8880  hi01t 8883  hi02t 8884  abshicomt 8888  hilabl 8948  bcsALT 8967  hhcms 8993  norm1t 9042  hhssnv 9054  hhssnvt 9055  hhsssh 9059  hhsscms 9067  pjthlem7 9140  pjthlem8 9141  pjvalt 9154  shscl 9196  chsupid 9226  chsupsn 9227  spanid 9232  chdmm2t 9364  chdmm3t 9365  chdmm4t 9366  chdmj2t 9368  chdmj3t 9369  chdmj4t 9370  elspansn2t 9406  spansneleq 9409  spansneleqOLD 9410  normcant 9416  pjspansnt 9417  fh1t 9478  fh2t 9479  osumlem2 9496  chsot 9506  pjsumt 9572  mayete3 9590  ho0valt 9593  hoaddass 9619  ho2co 9624  hoid1 9632  hoid1r 9633  homulid2t 9643  hosubdit 9651  hosub4t 9656  hosubsubt 9660  eigpos 9679  adjvalt 9731  adjval2t 9732  hmopadj2t 9781  bralnfnt 9788  nmopneg 9805  lnop0t 9806  lnopmult 9807  lnopaddmul 9813  lnopsubmul 9815  lnopmulsub 9816  homco2t 9817  lnopm 9840  lnophs 9841  lnopco 9843  lnopeq0 9847  nmopunt 9854  hmopst 9860  hmopmt 9861  nmbdoplb 9864  nmcoplb 9873  nmophm 9876  lnfnaddmul 9889  nmbdfnlb 9893  nmcfnlb 9902  nlelsh 9908  riesz3 9910  riesz4 9911  cnlnadjlem2 9916  adjaddt 9940  nmopcoadj 9948  branmfnt 9951  cnvbramult 9960  kbass5t 9965  leop2t 9969  leop3t 9970  leoprf2t 9972  leoprft 9973  idleop 9976  leopaddt 9977  leopmulit 9978  leopnmidt 9982  hmopidmcht 9992  hmopidmpjt 9993  pjadjco 10000  pjss1co 10002  pjss2co 10003  pjssum 10010  pjssdif2 10013  pjidmcot 10019  pjhmopidm 10020  dfpjopt 10021  elpjrnt 10027  pjclem4a 10036  pjclem4 10037  pjadj2co 10042  pj3lem1 10044  pj3s 10045  hstpytht 10066  hstoht 10069  st0 10086  strlem1 10087  strlem3a 10089  hstrlem3a 10097  golem1 10108  stcltrlem1 10113  dmdmdt 10137  dmdsl3t 10150  mdsl3t 10151  mdslmd3 10167  irredlem2 10226  atabs 10236  sumdmdlem2 10253  cdj3lem2 10267  ghomgrpilem2 10291  ghomgrplem 10294  ghomfo 10296  ghomid 10299  elgiso 10303  symggrpiOLD 10311  symggrpi 10313  cayleylem2 10317  cayleylem3 10318  11st22nd 10354  idhme 10409  hmeogrp 10425  mslb1 10473  msra3 10475  iint 10478  cnvtr 10482  domval 10499  codval 10500  idval 10501  cmpval 10502  eloi 10503  iscat 10531  cati 10532  ishomb 10560  cmpassoh 10573  homgrf 10574  isfuna 10592

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