Theorem eqtrid 2238

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 2226	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr2id  2239  eqtr3id  2240  3eqtr3a  2250  3eqtr4g  2251  csbtt  3092  csbvarg  3108  csbie2g  3131  rabbi2dva  3367  csbprc  3492  disjssun  3510  disjpr2  3682  prprc2  3727  difprsn2  3758  opprc  3825  intsng  3904  riinm  3985  iinxsng  3986  iunxprg  3993  rintm  4005  sucprc  4443  unisucg  4445  xpriindim  4800  relop  4812  dmxpm  4882  riinint  4923  resabs1  4971  resabs2  4973  resima2  4976  xpssres  4977  resopab2  4989  mptimass  5018  imasng  5030  ndmima  5042  xpdisj1  5090  xpdisj2  5091  djudisj  5093  resdisj  5094  rnxpm  5095  xpima1  5112  xpima2m  5113  dmsnsnsng  5143  rnsnopg  5144  rnpropg  5145  mptiniseg  5160  dfco2a  5166  relcoi1  5197  unixpm  5201  iotaval  5226  funtp  5307  fnun  5360  fnresdisj  5364  fnima  5372  fnimaeq0  5375  fcoi1  5434  f1orescnv  5516  foun  5519  resdif  5522  tz6.12-2  5545  fveu  5546  tz6.12-1  5581  fvun2  5624  fvopab3ig  5631  f1oresrab  5723  dfmptg  5737  ressnop0  5739  fvunsng  5752  fnsnsplitss  5757  fsnunfv  5759  fvpr1  5762  fvpr2  5763  fvpr1g  5764  fvpr2g  5765  fvtp1g  5766  fvtp2g  5767  fvtp3g  5768  fvtp2  5770  fvtp3  5771  f1oiso2  5870  riotaund  5908  ovprc  5953  resoprab2  6015  fnoprabg  6019  ovidig  6036  ovigg  6039  ov6g  6056  ovconst2  6070  offval2  6146  ot1stg  6205  ot2ndg  6206  ot3rdgg  6207  fmpoco  6269  algrflemg  6283  tpostpos2  6318  rdgisuc1  6437  frec0g  6450  frecsuclem  6459  frecrdg  6461  oasuc  6517  oa1suc  6520  omsuc  6525  nnm1  6578  nnm2  6579  dfec2  6590  errn  6609  ixpsnval  6755  ixpintm  6779  mapen  6902  xpmapenlem  6905  phplem2  6909  undifdc  6980  fisseneq  6988  ssfirab  6990  eqinfti  7079  infvalti  7081  infsnti  7089  casef  7147  caseinl  7150  caseinr  7151  djudom  7152  ctssdccl  7170  nninfwlpoimlemginf  7235  exmidfodomrlemim  7261  1qec  7448  mulidnq  7449  addpinq1  7524  suplocexprlem2b  7774  suplocexprlemlub  7784  0idsr  7827  1idsr  7828  caucvgsrlemoffres  7860  caucvgsr  7862  mulresr  7898  pitonnlem2  7907  ax1rid  7937  axcnre  7941  negid  8266  subneg  8268  negneg  8269  dfinfre  8975  2times  9110  infrenegsupex  9659  rexneg  9896  xaddpnf2  9913  xaddmnf1  9914  xaddmnf2  9915  fseq1p1m1  10160  fzosplitprm1  10301  intfracq  10391  frec2uz0d  10470  frec2uzrdg  10480  frecuzrdg0  10484  frecuzrdgg  10487  frecuzrdg0t  10493  seq3val  10531  seqvalcd  10532  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsum  10584  seqf1oglem2  10591  sqval  10668  iexpcyc  10715  binom3  10728  faclbnd  10812  faclbnd2  10813  bcn1  10829  hashinfom  10849  hashennn  10851  hashxp  10897  csbwrdg  10943  shftlem  10960  shftuz  10961  shftidt  10977  reim0  11005  remullem  11015  resqrexlemf1  11152  resqrexlemcalc3  11160  absexpzap  11224  absimle  11228  amgm2  11262  minmax  11373  mingeb  11385  2zinfmin  11386  xrmaxiflemval  11393  xrmaxadd  11404  infxrnegsupex  11406  xrminmax  11408  summodc  11526  fsum3  11530  sumsnf  11552  sumsns  11558  isumclim3  11566  isumge0  11573  fsump1i  11576  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fsumconst  11597  fsumiun  11620  hashrabrex  11624  hashuni  11625  binom11  11629  isumsplit  11634  geo2sum  11657  mertensabs  11680  prodmodc  11721  fprodseq  11726  prodsnf  11735  prodsns  11746  fprodconst  11763  fprod2dlemstep  11765  fprodcom2fi  11769  efgt1p2  11838  efgt1p  11839  resinval  11858  recosval  11859  cosadd  11880  ef01bndlem  11899  eirraplem  11920  nninfctlemfo  12177  ialgr0  12182  algrp1  12184  eucalg  12197  phiprmpw  12360  phiprm  12361  prmdiv  12373  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pceu  12433  pcfac  12488  prmpwdvds  12493  4sqlem5  12520  mul4sqlem  12531  ennnfonelem0  12562  ennnfonelemfun  12574  ennnfonelemf1  12575  ennnfonelemrn  12576  ctinfomlemom  12584  nninfdclemp1  12607  ndxid  12642  setsfun0  12654  setsresg  12656  setscom  12658  strslfv2d  12661  basm  12679  ressval3d  12690  resseqnbasd  12691  imasaddvallemg  12898  xpsval  12935  plusffvalg  12945  mgm1  12953  grpidvalg  12956  sgrp1  12994  mnd1  13027  mnd1id  13028  subsubm  13055  grppropstrg  13091  grpinvfvalg  13114  grpsubfvalg  13117  grp1  13178  mulgfvalg  13191  mulgnn0gsum  13198  mulg2  13201  subsubg  13267  releqgg  13290  eqgfval  13292  conjsubg  13347  gsumfzconstf  13412  mgpvalg  13419  mgpbasg  13422  mgpscag  13423  mgptopng  13425  mgpdsg  13426  mgpress  13427  ringidvalg  13457  ring1  13555  opprvalg  13565  opprmulfvalg  13566  opprbasg  13571  oppraddg  13572  subsubrng  13710  subsubrg  13741  rrgval  13758  scaffvalg  13802  lmodpropd  13845  lsssetm  13852  lsslss  13877  lspfval  13884  sraring  13945  lidlvalg  13967  rspvalg  13968  lidlss  13972  islidlm  13975  lidl0cl  13979  lidlacl  13980  lidlnegcl  13981  lidl0  13985  lidl1  13986  rspcl  13987  rspssid  13988  rsp0  13989  rspssp  13990  2idlval  13998  2idlvalg  13999  crngridl  14026  rspsn  14030  zrhval  14105  zrhvalg  14106  zlmval  14115  zlmbasg  14117  zlmplusgg  14118  zlmmulrg  14119  znval  14124  znzrh2  14134  znf1o  14139  psrval  14152  tgidm  14242  tgrest  14337  ssidcn  14378  txcnmpt  14441  txcn  14443  blres  14602  mopnval  14610  remetdval  14707  divccncfap  14745  cncfmet  14747  cncfcncntop  14748  hovergt0  14804  cnplimcim  14821  cnplimclemr  14823  limccnpcntop  14829  limccnp2cntop  14831  dvexp  14860  elply2  14881  elplyd  14887  plyaddlem1  14893  plymullem1  14894  sin0pilem1  14916  pilem3  14918  ef2kpi  14941  sin2pim  14948  cos2pim  14949  sinmpi  14950  cosmpi  14951  sinppi  14952  cosppi  14953  sinhalfpip  14955  sinhalfpim  14956  coshalfpip  14957  coshalfpim  14958  tangtx  14973  1cxp  15035  ecxp  15036  rplogb1  15080  rpelogb  15081  binom4  15111  lgslem1  15116  gausslemma2dlem4  15180  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2sqlem8  15210  ex-ceil  15218  qdencn  15517  cvgcmp2nlemabs  15522  trilpolemlt1  15531  nconstwlpolem0  15553