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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2id  2284  eqtr3id  2285  3eqtr3a  2295  3eqtr4g  2296  eqab  2373  csbtt  3159  csbvarg  3175  csbie2g  3198  rabbi2dva  3439  csbprc  3572  disjssun  3588  inssdif0im  3592  disjpr2  3773  rabsnif  3778  prprc2  3822  difprsn2  3855  opprc  3925  intsng  4004  riinm  4085  iinxsng  4086  iunxprg  4093  rintm  4105  sucprc  4557  unisucg  4559  xpriindim  4918  relop  4930  dmxpm  5002  riinint  5043  resabs1  5092  resabs2  5094  resima2  5097  xpssres  5098  resopab2  5110  mptimass  5139  imasng  5152  ndmima  5164  xpdisj1  5212  xpdisj2  5213  djudisj  5215  resdisj  5216  rnxpm  5217  xpima1  5234  xpima2m  5235  dmsnsnsng  5265  rnsnopg  5266  rnpropg  5267  mptiniseg  5282  dfco2a  5288  relcoi1  5319  unixpm  5323  iotaval  5349  funtp  5434  fnun  5489  fnresdisj  5493  fnima  5502  fnimaeq0  5505  fresaunres2disj  5570  fcoi1  5572  f1orescnv  5655  foun  5658  resdif  5661  tz6.12-2  5686  fveu  5687  tz6.12-1  5722  fvun2  5770  fvopab3ig  5779  f1oresrab  5873  dfmptg  5888  funopsn  5891  ressnop0  5896  fvunsng  5909  fnsnsplitss  5914  fsnunfv  5916  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvpr2g  5922  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  f1oiso2  6033  riotaund  6075  ovprc  6121  resoprab2  6185  fnoprabg  6189  ovidig  6206  ovigg  6209  fvmpopr2d  6225  ov6g  6227  ovconst2  6241  offval2  6318  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  opabn1stprc  6429  fmpoco  6452  algrflemg  6466  suppsnopdc  6490  tpostpos2  6536  rdgisuc1  6655  frec0g  6668  frecsuclem  6677  frecrdg  6679  oasuc  6737  oa1suc  6740  omsuc  6745  nnm1  6798  nnm2  6799  dfec2  6810  errn  6829  ixpsnval  6983  ixpintm  7007  mapen  7146  xpmapenlem  7149  phplem2  7154  undifdc  7231  prfidceq  7235  fisseneq  7242  ssfirab  7244  eqinfti  7361  infvalti  7363  infsnti  7371  casef  7429  caseinl  7432  caseinr  7433  djudom  7434  ctssdccl  7452  nninfwlpoimlemginf  7517  exmidfodomrlemim  7554  1qec  7756  mulidnq  7757  addpinq1  7832  suplocexprlem2b  8082  suplocexprlemlub  8092  0idsr  8135  1idsr  8136  caucvgsrlemoffres  8168  caucvgsr  8170  mulresr  8206  pitonnlem2  8215  ax1rid  8245  axcnre  8249  negid  8575  subneg  8577  negneg  8578  dfinfre  9289  2times  9435  infrenegsupex  10004  rexneg  10243  xaddpnf2  10260  xaddmnf1  10261  xaddmnf2  10262  fseq1p1m1  10512  fzosplitprm1  10664  infssfzcldc  10680  infssfzledc  10681  intfracq  10771  frec2uz0d  10850  frec2uzrdg  10860  frecuzrdg0  10864  frecuzrdgg  10867  frecuzrdg0t  10873  seq3val  10911  seqvalcd  10912  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  iseqf1olemfvp  10961  seq3f1olemqsum  10964  seqf1oglem2  10971  sqval  11048  iexpcyc  11095  binom3  11108  faclbnd  11194  faclbnd2  11195  bcn1  11211  hashinfom  11232  hashennn  11234  hashxp  11282  hashfibclem  11297  hashfibc  11298  hashf1lem1  11300  hashf1lem2  11301  hashtpgim  11312  hashtpglem  11313  hashtpg  11314  csbwrdg  11349  ccatlid  11389  s1val  11400  swrd00g  11436  pfxclz  11466  pfxccatpfx2  11524  cats1fvn  11551  cats1fvd  11553  cats1lend  11554  shftlem  11596  shftuz  11597  shftidt  11613  reim0  11641  remullem  11651  resqrexlemf1  11789  resqrexlemcalc3  11797  absexpzap  11862  absimle  11866  amgm2  11900  minmax  12013  mingeb  12026  2zinfmin  12027  xrmaxiflemval  12034  xrmaxadd  12045  infxrnegsupex  12047  xrminmax  12049  summodc  12168  fsum3  12172  sumsnf  12194  sumsns  12200  isumclim3  12208  isumge0  12215  fsump1i  12218  fsum2dlemstep  12219  fisumcom2  12223  fsumshftm  12230  fsumconst  12239  fsumiun  12262  hashrabrex  12266  hashuni  12267  binom11  12271  isumsplit  12276  geo2sum  12299  mertensabs  12322  prodmodc  12363  fprodseq  12368  prodsnf  12377  prodsns  12388  fprodconst  12405  fprod2dlemstep  12407  fprodcom2fi  12411  efgt1p2  12480  efgt1p  12481  resinval  12500  recosval  12501  cosadd  12522  ef01bndlem  12541  eirraplem  12562  bits0  12733  nninfctlemfo  12835  ialgr0  12840  algrp1  12842  eucalg  12855  phiprmpw  13022  phiprm  13023  prmdiv  13035  pythagtriplem12  13076  pythagtriplem14  13078  pythagtriplem16  13080  pceu  13096  pcfac  13151  prmpwdvds  13156  4sqlem5  13183  mul4sqlem  13194  ballotfilem4  13292  ballotfilem1c  13302  ballotfilemgun  13319  ennnfonelem0  13347  ennnfonelemfun  13359  ennnfonelemf1  13360  ennnfonelemrn  13361  ctinfomlemom  13369  nninfdclemp1  13392  ndxid  13427  setsfun0  13439  setsresg  13441  setscom  13443  strslfv2d  13446  basm  13465  ressval3d  13477  resseqnbasd  13478  imasaddvallemg  13687  plusffvalg  13733  mgm1  13741  grpidvalg  13744  sgrp1  13777  mnd1  13813  mnd1id  13814  subsubm  13841  grppropstrg  13875  grpinvfvalg  13898  grpsubfvalg  13901  grp1  13962  mulgfvalg  13975  mulgnn0gzsum  13982  mulg2  13985  subsubg  14051  releqgg  14074  eqgfval  14076  conjsubg  14131  gzsumconstf  14195  gsump1  14208  gsumclfi  14210  gsummptfidmadd  14212  gsumconstcmn  14217  prdsval  14224  prdsidlem  14244  prdsinvlem  14247  xpsval  14252  pwsval  14255  pwsplusgval  14259  pwsmulrval  14260  pwsinvg  14266  mgpvalg  14271  mgpbasg  14275  mgpscag  14277  mgptopng  14279  mgpdsg  14280  mgpress  14281  ringidvalg  14315  ring1  14415  opprvalg  14425  opprmulfvalg  14426  opprbasg  14431  oppraddg  14432  subsubrng  14573  subsubrg  14604  rrgval  14621  scaffvalg  14694  lmodpropd  14737  lsssetm  14744  lsslss  14769  lspfval  14776  sraring  14837  lidlvalg  14859  rspvalg  14860  lidlss  14864  islidlm  14867  lidl0cl  14871  lidlacl  14872  lidlnegcl  14873  lidl0  14877  lidl1  14878  rspcl  14879  rspssid  14880  rsp0  14881  rspssp  14882  2idlval  14890  2idlvalg  14891  crngridl  14918  rspsn  14922  zrhval  15003  zrhvalg  15004  zlmval  15013  zlmbasg  15015  zlmplusgg  15016  zlmmulrg  15017  znval  15022  znzrh2  15032  znf1o  15037  assapropd  15065  aspval  15066  psrval  15101  mplvalcoe  15133  mpl0fi  15145  mplnegfi  15148  tgidm  15227  tgrest  15322  ssidcn  15363  txcnmpt  15426  txcn  15428  blres  15587  mopnval  15595  remetdval  15700  expcn  15722  divccncfap  15743  cncfmet  15745  cncfcncntop  15746  hovergt0  15803  cnplimcim  15820  cnplimclemr  15822  limccnpcntop  15828  limccnp2cntop  15830  dvexp  15864  dvmptid  15869  dvmptfsum  15878  elply2  15888  elplyd  15894  plyaddlem1  15900  plymullem1  15901  plycjlemc  15913  sin0pilem1  15935  pilem3  15937  ef2kpi  15960  sin2pim  15967  cos2pim  15968  sinmpi  15969  cosmpi  15970  sinppi  15971  cosppi  15972  sinhalfpip  15974  sinhalfpim  15975  coshalfpip  15976  coshalfpim  15977  tangtx  15992  1cxp  16058  ecxp  16059  rplogb1  16106  rpelogb  16107  zprmlogbaplem2  16138  binom4  16141  log2tlbndlog2  16142  birthdaylem2  16148  birthdaylem3  16149  0sgm  16176  fsumdvdsmul  16207  1sgmprm  16210  1sgm2ppw  16211  ppiqub  16215  chtqub  16218  lgslem1  16241  gausslemma2dlem4  16305  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgseisenlem4  16314  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2lem1  16322  m1lgs  16326  2lgslem3a  16334  2lgslem3b  16335  2lgslem3c  16336  2lgslem3d  16337  2sqlem8  16364  opvtxov  16386  opiedgov  16389  structiedg0val  16403  edgov  16426  edg0iedg0g  16429  upgredg  16507  usgrf1oedg  16568  ushgredgedg  16589  ushgredgedgloop  16591  griedg0ssusgr  16614  subgrprop3  16625  0uhgrsubgr  16628  vtxdgfval  16651  vtxdfifiun  16660  vtxdumgrfival  16661  vtxd0nedgbfi  16662  1hevtxdg1en  16671  upgriswlkdc  16723  wlkres  16742  trlreslem  16752  clwwlkn2  16784  eupthvdres  16838  eupth2lem3fi  16839  ex-ceil  16862  depindlem1  16869  qdencn  17194  cvgcmp2nlemabs  17203  trilpolemlt1  17212  nconstwlpolem0  17235