Theorem eqtrd 1510

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
eqtrd.1	⊢ (φ → A = B)
eqtrd.2	⊢ (φ → B = C)

Assertion

Ref	Expression
eqtrd	⊢ (φ → A = C)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (φ → A = B)
2		eqtrd.2	. . 3 ⊢ (φ → B = C)
3	2	eqeq2d 1489	. 2 ⊢ (φ → (A = B ↔ A = C))
4	1, 3	mpbid 195	1 ⊢ (φ → A = C)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  eqtr2d 1511  eqtr3d 1512  eqtr4d 1513  3eqtrd 1514  3eqtr2d 1516  3eqtr3d 1518  3eqtr4d 1520  syl5eq 1522  syl6eq 1526  sylan9eq 1530  csbidmg 2042  csbco3g 2043  uneq12d 2188  ineq12d 2221  opeq1 2491  opeq12d 2499  hbopd 2501  opprc1 2502  csbopabg 2683  opprc3 2803  moop2 2807  unisn3 2882  suceq 3040  ordunisuc 3095  orduniss2 3096  onuninsuc 3114  xpid11 3341  hbimad 3418  csbima12g 3419  coi2 3517  funcnvres2 3576  fnco 3601  fco 3642  foima 3682  f1imacnv 3711  f1ococnv2 3714  hbfvd 3736  hbfvd2 3737  csbfv12g 3748  csbfv2g 3749  csbfvg 3750  funfv2 3777  fopabco 3838  fopabcos 3839  fvresi 3849  funiunfv 3872  tfrlem11 3927  tz7.44-2 3935  rdglem2 3944  rdglim2 3955  abianfplem 3967  opreq12d 3984  hboprd 3988  csboprg 3992  csbopr12g 3993  csbopr1g 3994  csbopr2g 3995  curry1 4104  curry1val 4106  eloprabi 4124  oev 4159  oa0 4161  oev2 4168  oa1suc 4170  om1r 4183  oaass 4201  odi 4216  omass 4217  oelim2 4228  nnmsucr 4246  nneob 4261  ereq 4273  oprec 4324  ecoprass 4326  ecoprdi 4327  pw2en 4452  mapenlem1 4495  mapenlem2 4496  mapxpen 4501  xpmapenlem3 4504  unfilem3 4562  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  opthreg 4613  r1val3 4689  rankxpsuc 4725  aceq5lem3 4747  aceq5lem4 4748  ac6lem 4764  kmlem9 4783  kmlem11 4785  kmlem12 4786  unidom 4818  unxpdomlem 4854  sucxpdom 4857  mulidpi 5026  addasspi 5035  mulasspi 5037  distrpi 5038  indpi 5046  mulidpq 5081  prlem934a 5149  prlem934b 5150  00sr 5220  recexsrlem 5224  mulresr 5269  ax0id 5293  ax1id 5294  axcnre 5298  addid2t 5341  add42t 5351  2addsubt 5401  pncant 5409  nppcant 5413  mulid2t 5429  muladd11t 5434  mul02t 5456  negdi2t 5468  subsubt 5474  nnncant 5478  mulm1t 5483  addsub4t 5485  pnpcant 5490  pnpcan2t 5491  recextlem1 5694  divcan2t 5733  recid2t 5743  divrec2t 5747  divcan4t 5764  dividt 5767  div0t 5768  divdivdivt 5787  recdivt 5792  lt2mul2divt 5874  nnmulclt 5943  times2t 6007  zltp1let 6183  nneo 6199  zneo 6202  uzindOLD 6210  quoremz 6253  fldivt 6256  uzrdgsuc 6305  seq1val 6313  seq1suclem 6317  ser1p1 6337  ser1add2 6339  ser1add 6340  shftval2t 6348  shftval4t 6350  shftval5t 6351  2shft 6353  shftcan2t 6354  iooval2t 6368  ioojoint 6417  fzshftralt 6523  seqzfval 6538  seqzvalt 6541  seq1seq02t 6544  seqzp1 6549  seq0p1 6552  seqzval2t 6554  ser0p1 6568  expvalt 6571  expnnvalt 6573  exp1t 6574  expp1t 6575  recexpt 6596  expmult 6598  sqvalt 6610  subsqt 6643  subsq2t 6644  bernneq 6653  discrlem3 6659  sqrmsq2 6707  sqsqr 6722  replimt 6762  imret 6774  reim0bt 6776  resubt 6806  imsubt 6809  cjsubt 6816  cjexpt 6817  imcjt 6819  absnegt 6832  absvalsqt 6835  absvalsq2t 6836  sqabsaddt 6848  sqabssubt 6849  absreimsqt 6856  absexpt 6868  cjdiv 6888  abssuble0t 6896  absmaxt 6897  abs1m 6904  recant 6905  ser1absdiflem 6929  faclbnd4lem4 6951  faclbnd6 6954  bcvalt 6958  bcn0t 6963  bcnp11t 6965  bcpasc 6969  sumeq12dv 6995  sumeq12rdv 6996  fsumserz 6999  fsum1p 7019  fsum2 7023  fsumcom 7028  fsumrev 7029  fsumrev2 7030  fsumshft 7031  fsumshftm 7032  fsummulc1 7033  fsum0 7039  fsumabs2mul 7044  ser1ser0 7048  serzrelem 7061  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binom1p 7073  bcxmas 7076  climshft2 7106  climaddlem3 7116  climsub 7130  iserzex 7146  climsup 7155  caucvg3a 7164  caucvg3lem 7166  ser1const 7171  ser10 7172  isumvalt 7192  fnsmntlem 7225  fnsmnt 7226  geoser 7234  geolimilem 7235  georeclim 7240  geosum 7241  cvgratlem1ALT 7247  cvgratlem1 7250  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag4 7261  negfcncf 7269  efcltlem2 7305  ef0lem 7310  erelem6 7324  efaddlem16 7353  efaddlem17 7354  efexpt 7372  eftabs 7375  ef1tllem 7381  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  abspef01tlub 7395  absefm1le 7412  resinvalt 7433  recosvalt 7434  efi4pt 7435  resin4pt 7436  recos4pt 7437  sinnegt 7442  cosnegt 7443  efmivalt 7448  sinsubt 7455  cossubt 7456  addsint 7457  subsint 7458  subcost 7460  sincossqt 7461  sin2tt 7462  cos01bndlem3 7472  absefit 7483  abseft 7484  demoivre 7485  demoivreALT 7486  acdc3lem 7487  acdc3 7488  acdc2lem1 7489  acdc2lem2 7490  acdc2 7491  acdc5lem1 7492  acdc5lem2 7493  acdc5 7494  acdclem 7495  acdc 7496  ruclem4 7514  infxpidmlem2 7554  infxpidmlem3 7555  alephsuc3 7587  ntrval 7673  clsval 7674  ntrval2 7683  neival 7714  lpval 7740  cnfval 7753  cnpfval 7754  cnpval 7756  idcn 7763  cncnplem4 7774  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metsym 7813  metreslem 7819  metxpdval 7826  metxpfval 7828  blfval 7832  blval 7834  blin 7849  cncfmet 7902  remetdval 7905  bl2ioo 7908  tgioolem 7911  lmconst 7931  lmfexlem2 7954  xpcn 7973  cncms 7995  bcthlem20 8015  isgrp 8038  grpidinvlem2 8046  grpidinv 8049  grpidval 8054  grpinvfval 8062  grpinvval 8063  grpdivfval 8077  grpdivval 8078  grpdivinv 8079  grpdivdiv 8083  grpdivid 8085  grpnpcan 8087  grpnnncan2 8089  grplactval 8093  abldivdiv 8104  ablnnncan 8107  ablnnncan1 8109  subgopr 8114  issubgi 8118  ablmul 8127  mulid 8128  isring 8137  ringi 8138  vci 8163  vcrinv 8187  vclinv 8188  vcsub4 8191  isvclem 8192  vcoprne 8194  vafval 8218  smfval 8220  0vfval 8221  invfval 8257  nvzs 8261  nvmdi 8266  nvrinv 8269  nvlinv 8270  nvpncan2 8272  nvaddsub4 8277  nvsge0 8287  nvm1 8288  nvabs 8297  nvop 8301  imsval 8312  imsdval 8313  imsdval2 8314  imsmetlem 8319  sqcn 8331  va1cnlem 8341  sm1cnilem 8343  ipfval 8348  ipval 8349  ipval2 8353  4ipval2 8354  ipval3 8355  4ipval3 8358  ipid 8359  ipcj 8363  ip0r 8366  sspmval 8388  sspival 8393  sspimsval 8395  lnoval 8409  lno0 8413  lnomul 8417  nmoval 8422  bloval 8437  0oval 8444  0lno 8446  nmo0 8447  blocnilem 8460  hmoval 8466  phop 8473  cnph 8474  ipasslem1 8486  ipasslem2 8487  ipasslem5 8490  ipasslem8 8493  ipdir 8498  ipdi 8499  ipass 8501  ipassr 8502  ipassr2 8503  ipsubdir 8504  ipsubdi 8505  sspph 8511  ubthlem8 8532  ubthlem9 8533  ubthlem10 8534  minveclem9 8549  minveclem18 8558  minveclem20 8560  minveclem23 8563  minveclem35 8575  htthlem5 8620  htthlem9 8624  isps 8641  spwval2 8649  spwval3 8650  spwnex3 8651  spwval 8655  sincolem 8660  sinmpi 8689  cosmpi 8690  sinppi 8691  sinkpi 8692  efimpi 8693  sinq12gt0t 8703  abssinper 8707  sineq0 8708  efgh 8713  efghgrpilem 8714  efif 8716  shftefif1olem 8736  efper 8742  relogexpt 8769  hvsubidt 8890  hv2negt 8892  hvaddsubvalt 8897  hvpncant 8903  hvsubdistr1t 8911  hvsub0t 8938  his52t 8949  his7t 8951  hiassdit 8952  his2subt 8953  his2sub2t 8954  hi01t 8957  hi02t 8958  abshicomt 8962  hilabl 9022  bcsALT 9041  hhcms 9067  norm1t 9116  hhssablt 9128  hhssnv 9129  hhssnvt 9130  hhsssh 9134  hhsscms 9145  pjthlem7 9220  pjthlem8 9221  pjvalt 9234  shscl 9276  chsupid 9306  chsupsn 9307  spanid 9312  chdmm2t 9444  chdmm3t 9445  chdmm4t 9446  chdmj2t 9448  chdmj3t 9449  chdmj4t 9450  elspansn2t 9485  spansneleq 9488  normcant 9494  pjspansnt 9495  fh1t 9556  fh2t 9557  osumlem2 9574  chsot 9584  pjsumt 9650  mayete3 9668  ho0valt 9671  hoaddass 9697  ho2co 9702  hoid1 9710  hoid1r 9711  homulid2t 9721  hosubdit 9729  hosub4t 9734  hosubsubt 9738  eigpos 9757  adjvalt 9809  adjval2t 9810  hmopadj2t 9860  bralnfnt 9867  nmopneg 9884  lnop0t 9885  lnopmult 9886  lnopaddmul 9892  lnopsubmul 9894  lnopmulsub 9895  homco2t 9896  lnopm 9920  lnophs 9921  lnopco 9923  lnopeq0 9927  nmopunt 9934  hmopst 9940  hmopmt 9941  nmbdoplb 9944  nmcoplb 9953  nmophm 9956  lnfnaddmul 9969  nmbdfnlb 9973  nmcfnlb 9982  nlelsh 9988  riesz3 9990  riesz4 9991  cnlnadjlem2 9996  adjaddt 10021  nmopcoadj 10029  branmfnt 10033  cnvbramult 10043  kbass5t 10048  leop2t 10052  leop3t 10053  leoprf2t 10055  leoprft 10056  idleop 10059  leopaddt 10060  leopmulit 10061  leopnmidt 10066  hmopidmcht 10076  hmopidmpjt 10077  pjadjco 10084  pjss1co 10086  pjss2co 10087  pjssum 10094  pjssdif2 10097  pjidmcot 10104  pjhmopidm 10105  dfpjopt 10106  elpjrnt 10112  pjclem4a 10121  pjclem4 10122  pjadj2co 10127  pj3lem1 10129  pj3s 10130  hstpytht 10151  hstoht 10154  st0 10171  strlem1 10172  strlem3a 10174  hstrlem3a 10182  golem1 10193  stcltrlem1 10198  dmdmdt 10222  dmdbr5 10230  dmdsl3t 10237  mdsl3t 10238  mdslmd3 10254  irredlem2 10313  atabs 10323  sumdmdlem2 10341  cdj3lem2 10357  ghomgrpilem2 10381  ghomgrplem 10384  ghomfo 10386  ghomid 10389  elgiso 10393  symggrpi 10401  cayleylem2 10405  cayleylem3 10406  11st22nd 10448  idhme 10508  hmeogrp 10524  sfvlim 10576  sfvlimOLD 10577  mslb1 10600  msra3 10602  iint 10605  cnvtr 10609  domval 10626  codval 10627  idval 10628  cmpval 10629  eloi 10630  iscat 10658  cati 10659  ishomb 10687  cmpassoh 10700  homgrf 10701  isepia 10718  isfuna 10725  idfisf 10731

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain