Theorem eqtrid 2283

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

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtr2id  2284  eqtr3id  2285  3eqtr3a  2295  3eqtr4g  2296  eqab  2373  csbtt  3159  csbvarg  3175  csbie2g  3198  rabbi2dva  3439  csbprc  3571  disjssun  3587  disjpr2  3769  rabsnif  3774  prprc2  3817  difprsn2  3850  opprc  3920  intsng  3999  riinm  4080  iinxsng  4081  iunxprg  4088  rintm  4100  sucprc  4552  unisucg  4554  xpriindim  4913  relop  4925  dmxpm  4997  riinint  5038  resabs1  5087  resabs2  5089  resima2  5092  xpssres  5093  resopab2  5105  mptimass  5134  imasng  5147  ndmima  5159  xpdisj1  5207  xpdisj2  5208  djudisj  5210  resdisj  5211  rnxpm  5212  xpima1  5229  xpima2m  5230  dmsnsnsng  5260  rnsnopg  5261  rnpropg  5262  mptiniseg  5277  dfco2a  5283  relcoi1  5314  unixpm  5318  iotaval  5344  funtp  5429  fnun  5484  fnresdisj  5488  fnima  5497  fnimaeq0  5500  fresaunres2disj  5565  fcoi1  5567  f1orescnv  5650  foun  5653  resdif  5656  tz6.12-2  5681  fveu  5682  tz6.12-1  5717  fvun2  5764  fvopab3ig  5773  f1oresrab  5864  dfmptg  5879  funopsn  5882  ressnop0  5887  fvunsng  5900  fnsnsplitss  5905  fsnunfv  5907  fvpr1  5910  fvpr2  5911  fvpr1g  5912  fvpr2g  5913  fvtp1g  5914  fvtp2g  5915  fvtp3g  5916  fvtp2  5918  fvtp3  5919  f1oiso2  6023  riotaund  6065  ovprc  6111  resoprab2  6175  fnoprabg  6179  ovidig  6196  ovigg  6199  fvmpopr2d  6215  ov6g  6217  ovconst2  6231  offval2  6308  ot1stg  6376  ot2ndg  6377  ot3rdgg  6378  opabn1stprc  6419  fmpoco  6442  algrflemg  6456  suppsnopdc  6480  tpostpos2  6526  rdgisuc1  6645  frec0g  6658  frecsuclem  6667  frecrdg  6669  oasuc  6727  oa1suc  6730  omsuc  6735  nnm1  6788  nnm2  6789  dfec2  6800  errn  6819  ixpsnval  6973  ixpintm  6997  mapen  7136  xpmapenlem  7139  phplem2  7144  undifdc  7221  prfidceq  7225  fisseneq  7232  ssfirab  7234  eqinfti  7350  infvalti  7352  infsnti  7360  casef  7418  caseinl  7421  caseinr  7422  djudom  7423  ctssdccl  7441  nninfwlpoimlemginf  7506  exmidfodomrlemim  7543  1qec  7745  mulidnq  7746  addpinq1  7821  suplocexprlem2b  8071  suplocexprlemlub  8081  0idsr  8124  1idsr  8125  caucvgsrlemoffres  8157  caucvgsr  8159  mulresr  8195  pitonnlem2  8204  ax1rid  8234  axcnre  8238  negid  8563  subneg  8565  negneg  8566  dfinfre  9276  2times  9411  infrenegsupex  9973  rexneg  10211  xaddpnf2  10228  xaddmnf1  10229  xaddmnf2  10230  fseq1p1m1  10479  fzosplitprm1  10631  infssfzcldc  10647  infssfzledc  10648  intfracq  10735  frec2uz0d  10814  frec2uzrdg  10824  frecuzrdg0  10828  frecuzrdgg  10831  frecuzrdg0t  10837  seq3val  10875  seqvalcd  10876  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsum  10928  seqf1oglem2  10935  sqval  11012  iexpcyc  11059  binom3  11072  faclbnd  11157  faclbnd2  11158  bcn1  11174  hashinfom  11195  hashennn  11197  hashxp  11245  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  hashtpgim  11275  hashtpglem  11276  hashtpg  11277  csbwrdg  11312  ccatlid  11352  s1val  11363  swrd00g  11399  pfxclz  11429  pfxccatpfx2  11487  cats1fvn  11514  cats1fvd  11516  cats1lend  11517  shftlem  11559  shftuz  11560  shftidt  11576  reim0  11604  remullem  11614  resqrexlemf1  11752  resqrexlemcalc3  11760  absexpzap  11824  absimle  11828  amgm2  11862  minmax  11974  mingeb  11986  2zinfmin  11987  xrmaxiflemval  11994  xrmaxadd  12005  infxrnegsupex  12007  xrminmax  12009  summodc  12128  fsum3  12132  sumsnf  12154  sumsns  12160  isumclim3  12168  isumge0  12175  fsump1i  12178  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fsumconst  12199  fsumiun  12222  hashrabrex  12226  hashuni  12227  binom11  12231  isumsplit  12236  geo2sum  12259  mertensabs  12282  prodmodc  12323  fprodseq  12328  prodsnf  12337  prodsns  12348  fprodconst  12365  fprod2dlemstep  12367  fprodcom2fi  12371  efgt1p2  12440  efgt1p  12441  resinval  12460  recosval  12461  cosadd  12482  ef01bndlem  12501  eirraplem  12522  bits0  12693  nninfctlemfo  12795  ialgr0  12800  algrp1  12802  eucalg  12815  phiprmpw  12978  phiprm  12979  prmdiv  12991  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pceu  13052  pcfac  13107  prmpwdvds  13112  4sqlem5  13139  mul4sqlem  13150  ballotfilem4  13219  ballotfilem1c  13229  ballotfilemgun  13246  ennnfonelem0  13274  ennnfonelemfun  13286  ennnfonelemf1  13287  ennnfonelemrn  13288  ctinfomlemom  13296  nninfdclemp1  13319  ndxid  13354  setsfun0  13366  setsresg  13368  setscom  13370  strslfv2d  13373  basm  13392  ressval3d  13403  resseqnbasd  13404  imasaddvallemg  13613  plusffvalg  13659  mgm1  13667  grpidvalg  13670  sgrp1  13703  mnd1  13739  mnd1id  13740  subsubm  13767  grppropstrg  13801  grpinvfvalg  13824  grpsubfvalg  13827  grp1  13888  mulgfvalg  13901  mulgnn0gzsum  13908  mulg2  13911  subsubg  13977  releqgg  14000  eqgfval  14002  conjsubg  14057  gzsumconstf  14121  gsump1  14134  gsumclfi  14136  gsummptfidmadd  14138  gsumconstcmn  14143  prdsval  14150  prdsidlem  14170  prdsinvlem  14173  xpsval  14178  pwsval  14181  pwsplusgval  14185  pwsmulrval  14186  pwsinvg  14192  mgpvalg  14197  mgpbasg  14200  mgpscag  14201  mgptopng  14203  mgpdsg  14204  mgpress  14205  ringidvalg  14239  ring1  14337  opprvalg  14347  opprmulfvalg  14348  opprbasg  14353  oppraddg  14354  subsubrng  14495  subsubrg  14526  rrgval  14543  scaffvalg  14615  lmodpropd  14658  lsssetm  14665  lsslss  14690  lspfval  14697  sraring  14758  lidlvalg  14780  rspvalg  14781  lidlss  14785  islidlm  14788  lidl0cl  14792  lidlacl  14793  lidlnegcl  14794  lidl0  14798  lidl1  14799  rspcl  14800  rspssid  14801  rsp0  14802  rspssp  14803  2idlval  14811  2idlvalg  14812  crngridl  14839  rspsn  14843  zrhval  14924  zrhvalg  14925  zlmval  14934  zlmbasg  14936  zlmplusgg  14937  zlmmulrg  14938  znval  14943  znzrh2  14953  znf1o  14958  psrval  14973  mplvalcoe  15004  mpl0fi  15016  mplnegfi  15019  tgidm  15098  tgrest  15193  ssidcn  15234  txcnmpt  15297  txcn  15299  blres  15458  mopnval  15466  remetdval  15571  expcn  15593  divccncfap  15614  cncfmet  15616  cncfcncntop  15617  hovergt0  15674  cnplimcim  15691  cnplimclemr  15693  limccnpcntop  15699  limccnp2cntop  15701  dvexp  15735  dvmptid  15740  dvmptfsum  15749  elply2  15759  elplyd  15765  plyaddlem1  15771  plymullem1  15772  plycjlemc  15784  sin0pilem1  15805  pilem3  15807  ef2kpi  15830  sin2pim  15837  cos2pim  15838  sinmpi  15839  cosmpi  15840  sinppi  15841  cosppi  15842  sinhalfpip  15844  sinhalfpim  15845  coshalfpip  15846  coshalfpim  15847  tangtx  15862  1cxp  15925  ecxp  15926  rplogb1  15973  rpelogb  15974  binom4  16004  0sgm  16013  fsumdvdsmul  16019  1sgmprm  16022  1sgm2ppw  16023  lgslem1  16033  gausslemma2dlem4  16097  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  m1lgs  16118  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2sqlem8  16156  opvtxov  16178  opiedgov  16181  structiedg0val  16195  edgov  16218  edg0iedg0g  16221  upgredg  16299  usgrf1oedg  16360  ushgredgedg  16381  ushgredgedgloop  16383  griedg0ssusgr  16406  subgrprop3  16417  0uhgrsubgr  16420  vtxdgfval  16443  vtxdfifiun  16452  vtxdumgrfival  16453  vtxd0nedgbfi  16454  1hevtxdg1en  16463  upgriswlkdc  16515  wlkres  16534  trlreslem  16544  clwwlkn2  16576  eupthvdres  16630  eupth2lem3fi  16631  ex-ceil  16654  depindlem1  16661  qdencn  16977  cvgcmp2nlemabs  16986  trilpolemlt1  16995  nconstwlpolem0  17018