Theorem eqtrid 2250

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqtrid.1	|- A = B
eqtrid.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtrid	|- ( ph -> A = C )

Proof of Theorem eqtrid

Step	Hyp	Ref	Expression
1		eqtrid.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		eqtrid.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrd 2238	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  eqtr2id  2251  eqtr3id  2252  3eqtr3a  2262  3eqtr4g  2263  csbtt  3105  csbvarg  3121  csbie2g  3144  rabbi2dva  3381  csbprc  3506  disjssun  3524  disjpr2  3697  prprc2  3742  difprsn2  3773  opprc  3840  intsng  3919  riinm  4000  iinxsng  4001  iunxprg  4008  rintm  4020  sucprc  4460  unisucg  4462  xpriindim  4817  relop  4829  dmxpm  4899  riinint  4940  resabs1  4989  resabs2  4991  resima2  4994  xpssres  4995  resopab2  5007  mptimass  5036  imasng  5048  ndmima  5060  xpdisj1  5108  xpdisj2  5109  djudisj  5111  resdisj  5112  rnxpm  5113  xpima1  5130  xpima2m  5131  dmsnsnsng  5161  rnsnopg  5162  rnpropg  5163  mptiniseg  5178  dfco2a  5184  relcoi1  5215  unixpm  5219  iotaval  5244  funtp  5328  fnun  5383  fnresdisj  5387  fnima  5396  fnimaeq0  5399  fcoi1  5458  f1orescnv  5540  foun  5543  resdif  5546  tz6.12-2  5569  fveu  5570  tz6.12-1  5605  fvun2  5648  fvopab3ig  5655  f1oresrab  5747  dfmptg  5761  funopsn  5764  ressnop0  5767  fvunsng  5780  fnsnsplitss  5785  fsnunfv  5787  fvpr1  5790  fvpr2  5791  fvpr1g  5792  fvpr2g  5793  fvtp1g  5794  fvtp2g  5795  fvtp3g  5796  fvtp2  5798  fvtp3  5799  f1oiso2  5898  riotaund  5936  ovprc  5982  resoprab2  6044  fnoprabg  6048  ovidig  6065  ovigg  6068  fvmpopr2d  6084  ov6g  6086  ovconst2  6100  offval2  6176  ot1stg  6240  ot2ndg  6241  ot3rdgg  6242  fmpoco  6304  algrflemg  6318  tpostpos2  6353  rdgisuc1  6472  frec0g  6485  frecsuclem  6494  frecrdg  6496  oasuc  6552  oa1suc  6555  omsuc  6560  nnm1  6613  nnm2  6614  dfec2  6625  errn  6644  ixpsnval  6790  ixpintm  6814  mapen  6945  xpmapenlem  6948  phplem2  6952  undifdc  7023  prfidceq  7027  fisseneq  7033  ssfirab  7035  eqinfti  7124  infvalti  7126  infsnti  7134  casef  7192  caseinl  7195  caseinr  7196  djudom  7197  ctssdccl  7215  nninfwlpoimlemginf  7280  exmidfodomrlemim  7311  1qec  7503  mulidnq  7504  addpinq1  7579  suplocexprlem2b  7829  suplocexprlemlub  7839  0idsr  7882  1idsr  7883  caucvgsrlemoffres  7915  caucvgsr  7917  mulresr  7953  pitonnlem2  7962  ax1rid  7992  axcnre  7996  negid  8321  subneg  8323  negneg  8324  dfinfre  9031  2times  9166  infrenegsupex  9717  rexneg  9954  xaddpnf2  9971  xaddmnf1  9972  xaddmnf2  9973  fseq1p1m1  10218  fzosplitprm1  10365  intfracq  10467  frec2uz0d  10546  frec2uzrdg  10556  frecuzrdg0  10560  frecuzrdgg  10563  frecuzrdg0t  10569  seq3val  10607  seqvalcd  10608  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsum  10660  seqf1oglem2  10667  sqval  10744  iexpcyc  10791  binom3  10804  faclbnd  10888  faclbnd2  10889  bcn1  10905  hashinfom  10925  hashennn  10927  hashxp  10973  csbwrdg  11025  ccatlid  11065  s1val  11074  swrd00g  11105  shftlem  11160  shftuz  11161  shftidt  11177  reim0  11205  remullem  11215  resqrexlemf1  11352  resqrexlemcalc3  11360  absexpzap  11424  absimle  11428  amgm2  11462  minmax  11574  mingeb  11586  2zinfmin  11587  xrmaxiflemval  11594  xrmaxadd  11605  infxrnegsupex  11607  xrminmax  11609  summodc  11727  fsum3  11731  sumsnf  11753  sumsns  11759  isumclim3  11767  isumge0  11774  fsump1i  11777  fsum2dlemstep  11778  fisumcom2  11782  fsumshftm  11789  fsumconst  11798  fsumiun  11821  hashrabrex  11825  hashuni  11826  binom11  11830  isumsplit  11835  geo2sum  11858  mertensabs  11881  prodmodc  11922  fprodseq  11927  prodsnf  11936  prodsns  11947  fprodconst  11964  fprod2dlemstep  11966  fprodcom2fi  11970  efgt1p2  12039  efgt1p  12040  resinval  12059  recosval  12060  cosadd  12081  ef01bndlem  12100  eirraplem  12121  bits0  12292  nninfctlemfo  12394  ialgr0  12399  algrp1  12401  eucalg  12414  phiprmpw  12577  phiprm  12578  prmdiv  12590  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pceu  12651  pcfac  12706  prmpwdvds  12711  4sqlem5  12738  mul4sqlem  12749  ennnfonelem0  12809  ennnfonelemfun  12821  ennnfonelemf1  12822  ennnfonelemrn  12823  ctinfomlemom  12831  nninfdclemp1  12854  ndxid  12889  setsfun0  12901  setsresg  12903  setscom  12905  strslfv2d  12908  basm  12926  ressval3d  12937  resseqnbasd  12938  prdsval  13138  pwsval  13156  pwsplusgval  13160  pwsmulrval  13161  imasaddvallemg  13180  xpsval  13217  plusffvalg  13227  mgm1  13235  grpidvalg  13238  sgrp1  13276  prdsidlem  13312  mnd1  13320  mnd1id  13321  subsubm  13348  grppropstrg  13384  grpinvfvalg  13407  grpsubfvalg  13410  grp1  13471  prdsinvlem  13473  pwsinvg  13477  mulgfvalg  13490  mulgnn0gsum  13497  mulg2  13500  subsubg  13566  releqgg  13589  eqgfval  13591  conjsubg  13646  gsumfzconstf  13711  mgpvalg  13718  mgpbasg  13721  mgpscag  13722  mgptopng  13724  mgpdsg  13725  mgpress  13726  ringidvalg  13756  ring1  13854  opprvalg  13864  opprmulfvalg  13865  opprbasg  13870  oppraddg  13871  subsubrng  14009  subsubrg  14040  rrgval  14057  scaffvalg  14101  lmodpropd  14144  lsssetm  14151  lsslss  14176  lspfval  14183  sraring  14244  lidlvalg  14266  rspvalg  14267  lidlss  14271  islidlm  14274  lidl0cl  14278  lidlacl  14279  lidlnegcl  14280  lidl0  14284  lidl1  14285  rspcl  14286  rspssid  14287  rsp0  14288  rspssp  14289  2idlval  14297  2idlvalg  14298  crngridl  14325  rspsn  14329  zrhval  14412  zrhvalg  14413  zlmval  14422  zlmbasg  14424  zlmplusgg  14425  zlmmulrg  14426  znval  14431  znzrh2  14441  znf1o  14446  psrval  14461  mplvalcoe  14485  mpl0fi  14497  mplnegfi  14500  tgidm  14579  tgrest  14674  ssidcn  14715  txcnmpt  14778  txcn  14780  blres  14939  mopnval  14947  remetdval  15052  expcn  15074  divccncfap  15095  cncfmet  15097  cncfcncntop  15098  hovergt0  15155  cnplimcim  15172  cnplimclemr  15174  limccnpcntop  15180  limccnp2cntop  15182  dvexp  15216  dvmptid  15221  dvmptfsum  15230  elply2  15240  elplyd  15246  plyaddlem1  15252  plymullem1  15253  plycjlemc  15265  sin0pilem1  15286  pilem3  15288  ef2kpi  15311  sin2pim  15318  cos2pim  15319  sinmpi  15320  cosmpi  15321  sinppi  15322  cosppi  15323  sinhalfpip  15325  sinhalfpim  15326  coshalfpip  15327  coshalfpim  15328  tangtx  15343  1cxp  15405  ecxp  15406  rplogb1  15453  rpelogb  15454  binom4  15484  0sgm  15490  fsumdvdsmul  15496  1sgmprm  15499  1sgm2ppw  15500  lgslem1  15510  gausslemma2dlem4  15574  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem1  15591  m1lgs  15595  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2sqlem8  15633  opvtxov  15653  opiedgov  15656  structiedg0val  15670  edgov  15690  edg0iedg0g  15693  ex-ceil  15699  qdencn  16003  cvgcmp2nlemabs  16008  trilpolemlt1  16017  nconstwlpolem0  16039