Theorem eqtrd 1128

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

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  eqtr2d 1129  eqtr3d 1130  eqtr4d 1131  3eqtrd 1132  3eqtr3d 1133  3eqtr4d 1134  syl5eq 1136  syl6eq 1140  sylan9eq 1144  uneq12d 1612  ineq12d 1646  opeq1 1876  opprc1 1905  opprc3 1908  moop2 1910  suceq 2288  ordunisuc 2339  onuninsuc 2356  coi2 2666  funimacnv 2711  fco 2760  foima 2790  f1imacnv 2814  f1ococnv2 2817  funfv2 2863  fvresi 2901  tfrlem11 2959  tz7.44-2 2967  rdglem2 2976  rdglim2 2987  abianfplem 2999  opreq12d 3014  oev 3122  oa0 3124  oa1suc 3132  om1r 3145  oaass 3163  nndi 3180  nnmass 3181  nnmsucr 3182  ereq 3206  oprec 3254  ecoprass 3256  ecoprdi 3257  pw2en 3348  mapenlem1 3384  mapenlem2 3385  mapxpen 3390  xpmapenlem3 3393  unfilem3 3440  fiint 3445  r1val3 3523  aceq5lem3 3560  aceq5lem4 3561  ac6lem 3575  kmlem8 3587  kmlem10 3589  kmlem11 3590  fodomb 3615  unxpdomlem 3649  sucxpdom 3652  mulidpi 3808  addasspi 3817  mulasspi 3819  distrpi 3820  indpi 3828  mulidpq 3863  prlem934a 3931  prlem934b 3932  00sr 4002  recexsrlem 4006  mulresr 4051  ax0id 4076  ax1id 4077  axrecex 4079  axcnre 4087  addid2t 4132  subneg2t 4158  pncant 4161  mulid2t 4175  mulzer2t 4189  mulm1t 4204  divdivdivt 4265  nnmulclt 4437  zneo 4601  uzind 4603  uzrdgsuc 4659  seqval 4665  seqsuclem 4669  expp1t 4678  exp1t 4679  exp2t 4683  discrlem3 4715  nneo 4719  sqrsq 4764  sqsqr 4775  replimt 4798  ruclem4 4888  infxpidmlem2 4934  infxpidmlem3 4935  alephsuc3 4955  hvsubidt 5005  hvsubcan1t 5016  hvsubcan2t 5017  hvsub0t 5041  his7 5051  his2subt 5052  hizer1t 5054  hizer2t 5055  bcs 5101  pjthlem7 5231  pjthlem8 5232  pjvalt 5246  chsupsn 5313  chdmm2t 5439  chdmm3t 5440  chdmm4t 5441  chdmj2t 5443  chdmj3t 5444  chdmj4t 5445  elspansn2t 5472  spansneleq 5475  osumlem2 5531  pjch0t 5562  pjsumt 5590  hosass 5607  ho2co 5611  hoid1 5617  hoid1r 5618  pjadjco 5631  pjss1co 5633  pjss2co 5634  pjssum 5641  pjclem2 5650  pjclem4a 5652  pjclem4 5653  pjadj2co 5656  pj3lem1 5658  pj3s 5659  st0 5690  strlem1 5691  strlem3a 5693  golem1 5704  stcltrlem1 5709  dmdbr 5731

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org