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  4559  unisucg  4561  xpriindim  4920  relop  4932  dmxpm  5004  riinint  5045  resabs1  5094  resabs2  5096  resima2  5099  xpssres  5100  resopab2  5113  mptimass  5142  imasng  5155  ndmima  5167  xpdisj1  5215  xpdisj2  5216  djudisj  5218  resdisj  5219  rnxpm  5220  xpima1  5237  xpima2m  5238  dmsnsnsng  5268  rnsnopg  5269  rnpropg  5270  mptiniseg  5285  dfco2a  5291  relcoi1  5322  unixpm  5326  iotaval  5352  funtp  5437  fnun  5492  fnresdisj  5496  fnima  5505  fnimaeq0  5508  fresaunres2disj  5573  fcoi1  5575  f1orescnv  5658  foun  5661  resdif  5664  tz6.12-2  5689  fveu  5690  tz6.12-1  5725  fvun2  5773  fvopab3ig  5782  f1oresrab  5876  dfmptg  5891  funopsn  5894  ressnop0  5899  fvunsng  5912  fnsnsplitss  5917  fsnunfv  5919  fvpr1  5922  fvpr2  5923  fvpr1g  5924  fvpr2g  5925  fvtp1g  5926  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  f1oiso2  6036  riotaund  6078  ovprc  6124  resoprab2  6188  fnoprabg  6192  ovidig  6209  ovigg  6212  fvmpopr2d  6228  ov6g  6230  ovconst2  6244  offval2  6322  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  opabn1stprc  6433  fmpoco  6456  algrflemg  6470  suppsnopdc  6494  tpostpos2  6541  rdgisuc1  6660  frec0g  6673  frecsuclem  6682  frecrdg  6684  oasuc  6742  oa1suc  6745  omsuc  6750  nnm1  6803  nnm2  6804  dfec2  6815  errn  6834  ixpsnval  6989  ixpintm  7013  mapen  7152  xpmapenlem  7155  phplem2  7160  undifdc  7237  prfidceq  7241  fisseneq  7248  ssfirab  7250  eqinfti  7366  infvalti  7368  infsnti  7376  casef  7434  caseinl  7437  caseinr  7438  djudom  7439  ctssdccl  7457  nninfwlpoimlemginf  7522  exmidfodomrlemim  7559  1qec  7761  mulidnq  7762  addpinq1  7837  suplocexprlem2b  8087  suplocexprlemlub  8097  0idsr  8140  1idsr  8141  caucvgsrlemoffres  8173  caucvgsr  8175  mulresr  8211  pitonnlem2  8220  ax1rid  8250  axcnre  8254  negid  8580  subneg  8582  negneg  8583  dfinfre  9294  2times  9441  infrenegsupex  10009  rexneg  10248  xaddpnf2  10265  xaddmnf1  10266  xaddmnf2  10267  fseq1p1m1  10517  fzosplitprm1  10669  infssfzcldc  10685  infssfzledc  10686  intfracq  10777  frec2uz0d  10856  frec2uzrdg  10866  frecuzrdg0  10870  frecuzrdgg  10873  frecuzrdg0t  10879  seq3val  10917  seqvalcd  10918  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsum  10970  seqf1oglem2  10977  sqval  11054  iexpcyc  11101  binom3  11114  faclbnd  11200  faclbnd2  11201  bcn1  11217  hashinfom  11238  hashennn  11240  hashxp  11288  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  hashtpgim  11318  hashtpglem  11319  hashtpg  11320  csbwrdg  11355  ccatlid  11395  s1val  11406  swrd00g  11442  pfxclz  11472  pfxccatpfx2  11530  cats1fvn  11557  cats1fvd  11559  cats1lend  11560  shftlem  11602  shftuz  11603  shftidt  11619  reim0  11647  remullem  11657  resqrexlemf1  11795  resqrexlemcalc3  11803  absexpzap  11868  absimle  11872  amgm2  11906  minmax  12019  mingeb  12032  2zinfmin  12033  xrmaxiflemval  12040  xrmaxadd  12051  infxrnegsupex  12053  xrminmax  12055  summodc  12174  fsum3  12178  sumsnf  12200  sumsns  12206  isumclim3  12214  isumge0  12221  fsump1i  12224  fsum2dlemstep  12225  fisumcom2  12229  fsumshftm  12236  fsumconst  12245  fsumiun  12268  hashrabrex  12272  hashuni  12273  binom11  12277  isumsplit  12282  geo2sum  12305  mertensabs  12328  prodmodc  12369  fprodseq  12374  prodsnf  12383  prodsns  12394  fprodconst  12411  fprod2dlemstep  12413  fprodcom2fi  12417  efgt1p2  12486  efgt1p  12487  resinval  12506  recosval  12507  cosadd  12528  ef01bndlem  12547  eirraplem  12568  bits0  12739  nninfctlemfo  12841  ialgr0  12846  algrp1  12848  eucalg  12861  phiprmpw  13028  phiprm  13029  prmdiv  13041  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  pceu  13102  pcfac  13157  prmpwdvds  13162  4sqlem5  13189  mul4sqlem  13200  ballotfilem4  13298  ballotfilem1c  13308  ballotfilemgun  13325  ennnfonelem0  13353  ennnfonelemfun  13365  ennnfonelemf1  13366  ennnfonelemrn  13367  ctinfomlemom  13375  nninfdclemp1  13398  ndxid  13433  setsfun0  13445  setsresg  13447  setscom  13449  strslfv2d  13452  basm  13471  ressval3d  13484  resseqnbasd  13485  imasaddvallemg  13694  plusffvalg  13740  mgm1  13748  grpidvalg  13751  sgrp1  13784  mnd1  13820  mnd1id  13821  subsubm  13848  grppropstrg  13882  grpinvfvalg  13905  grpsubfvalg  13908  grp1  13969  mulgfvalg  13982  mulgnn0gzsum  13989  mulg2  13992  subsubg  14058  releqgg  14081  eqgfval  14083  conjsubg  14138  cntzfval  14151  gzsumconstf  14233  gsump1  14246  gsumclfi  14248  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsummptfidmsplitres  14254  gsumsnfdcmn  14256  gsumresfi  14262  gsumconstcmn  14265  gsum2d2fi  14273  prdsval  14279  prdsidlem  14299  prdsinvlem  14302  xpsval  14307  pwsval  14310  pwsplusgval  14314  pwsmulrval  14315  pwsinvg  14321  mgpvalg  14326  mgpbasg  14330  mgpscag  14332  mgptopng  14334  mgpdsg  14335  mgpress  14336  ringidvalg  14370  ring1  14470  opprvalg  14482  opprmulfvalg  14483  opprbasg  14488  oppraddg  14489  subsubrng  14630  subsubrg  14661  rrgval  14678  scaffvalg  14751  lmodpropd  14794  lsssetm  14801  lsslss  14826  lspfval  14833  sraring  14894  lidlvalg  14916  rspvalg  14917  lidlss  14921  islidlm  14924  lidl0cl  14928  lidlacl  14929  lidlnegcl  14930  lidl0  14934  lidl1  14935  rspcl  14936  rspssid  14937  rsp0  14938  rspssp  14939  2idlval  14947  2idlvalg  14948  crngridl  14975  rspsn  14979  zrhval  15060  zrhvalg  15061  zlmval  15070  zlmbasg  15072  zlmplusgg  15073  zlmmulrg  15074  znval  15079  znzrh2  15089  znf1o  15094  assapropd  15122  aspval  15123  psrval  15160  psrass1filem  15186  mvrfval  15214  mplvalg  15222  mpl0fi  15235  mplnegfi  15238  tgidm  15317  tgrest  15412  ssidcn  15453  txcnmpt  15516  txcn  15518  blres  15677  mopnval  15685  remetdval  15790  expcn  15812  divccncfap  15833  cncfmet  15835  cncfcncntop  15836  hovergt0  15893  cnplimcim  15910  cnplimclemr  15912  limccnpcntop  15918  limccnp2cntop  15920  dvexp  15954  dvmptid  15959  dvmptfsum  15968  elply2  15978  elplyd  15984  plyaddlem1  15990  plymullem1  15991  plycjlemc  16003  sin0pilem1  16025  pilem3  16027  ef2kpi  16050  sin2pim  16057  cos2pim  16058  sinmpi  16059  cosmpi  16060  sinppi  16061  cosppi  16062  sinhalfpip  16064  sinhalfpim  16065  coshalfpip  16066  coshalfpim  16067  tangtx  16082  1cxp  16150  ecxp  16151  rplogb1  16201  rpelogb  16202  zprmlogbaplem2  16233  binom4  16236  log2tlbndlog2  16237  birthdaylem2  16243  birthdaylem3  16244  0sgm  16271  fsumdvdsmul  16302  1sgmprm  16305  1sgm2ppw  16306  ppiqub  16310  chtqub  16313  bposlem9  16336  lgslem1  16341  gausslemma2dlem4  16405  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  m1lgs  16426  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2sqlem8  16464  opvtxov  16486  opiedgov  16489  structiedg0val  16503  edgov  16526  edg0iedg0g  16529  upgredg  16607  usgrf1oedg  16668  ushgredgedg  16689  ushgredgedgloop  16691  griedg0ssusgr  16714  subgrprop3  16725  0uhgrsubgr  16728  vtxdgfval  16751  vtxdfifiun  16760  vtxdumgrfival  16761  vtxd0nedgbfi  16762  1hevtxdg1en  16771  upgriswlkdc  16823  wlkres  16842  trlreslem  16852  clwwlkn2  16884  eupthvdres  16938  eupth2lem3fi  16939  ex-ceil  16962  depindlem1  16969  idjudju  17269  qdencn  17295  cvgcmp2nlemabs  17304  trilpolemlt1  17314  nconstwlpolem0  17337