Theorem eqtrdi 2254

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem eqtrdi

Step	Hyp	Ref	Expression
1		eqtrdi.1	. 2 |- ( ph -> A = B )
2		eqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 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:  eqtr2di  2255  eqtr4di  2256  3eqtr3g  2261  3eqtr4a  2264  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  csbprc  3506  un00  3507  disjssun  3524  disjpr2  3697  tppreq3  3736  diftpsn3  3774  preq12b  3811  intsng  3919  uniintsnr  3921  rint0  3924  riin0  3999  iununir  4011  intexr  4195  exmid1stab  4253  sucprc  4460  op1stbg  4527  elreldm  4905  xpeq0r  5106  xpdisj1  5108  xpdisj2  5109  resdisj  5112  xpima1  5130  xpima2m  5131  elxp4  5171  unixp0im  5220  uniabio  5243  iotass  5250  cnvresid  5349  funimacnv  5351  fimadmfo  5509  f1o00  5559  dffv4g  5575  fv2prc  5615  fnrnfv  5627  feqresmpt  5635  dffn5imf  5636  funfvdm2f  5646  fvun1  5647  fvmpt2  5665  fndmin  5689  fmptcof  5749  fmptcos  5750  funopdmsn  5766  fvunsng  5780  fvpr1  5790  fnrnov  6094  offval  6168  ofrfval  6169  op1std  6236  op2ndd  6237  fmpoco  6304  tpostpos  6352  tfr0  6411  rdgival  6470  frec0g  6485  2oconcl  6527  om0  6546  oei0  6547  oasuc  6552  omv2  6553  nnm0r  6567  uniqs2  6684  en1  6893  en1bg  6894  fundmen  6900  mapsnen  6905  en2  6914  xpsnen  6918  xpcomco  6923  xpdom2  6928  xpmapenlem  6948  exmidpweq  7008  unsnfidcex  7019  fiintim  7030  ssfirab  7035  sbthlemi8  7068  elfi2  7076  fi0  7079  fieq0  7080  djudom  7197  ismkvnex  7259  nninfwlpoimlemg  7279  en2other2  7306  exmidfodomrlemim  7311  nq0m0r  7571  addpinq1  7579  genipv  7624  genpelvl  7627  genpelvu  7628  cauappcvgprlem1  7774  caucvgsrlemoffres  7915  addresr  7952  mulresr  7953  axcnre  7996  add20  8549  rimul  8660  rereim  8661  mulreim  8679  sup3exmid  9032  fv0p1e1  9153  div4p1lem1div2  9293  nnm1nn0  9338  znegcl  9405  peano2z  9410  nneoor  9477  nn0ind-raph  9492  xnegneg  9957  xltnegi  9959  xaddpnf1  9970  xnegid  9983  xnn0xadd0  9991  xnegdi  9992  xsubge0  10005  xposdif  10006  xlesubadd  10007  xleaddadd  10011  fz0to4untppr  10248  fzo0to2pr  10349  nninfdcex  10382  fldiv4p1lem1div2  10450  fldiv4lem1div2  10452  mulp1mod1  10512  frecfzennn  10573  iseqf1olemqk  10654  exp0  10690  expp1  10693  expnegap0  10694  1exp  10715  mulexp  10725  m1expeven  10733  sq0i  10778  bernneq  10807  facp1  10877  faclbnd3  10890  facubnd  10892  bcval5  10910  hashinfom  10925  hashsng  10945  hashxp  10973  resunimafz0  10978  zfz1iso  10988  hash2en  10990  lsw1  11045  s1rn  11075  eqs1  11085  ccat1st1st  11096  swrd00g  11105  swrdlend  11114  swrds1  11124  imre  11195  reim0b  11206  rereb  11207  resqrexlemover  11354  resqrexlemcalc1  11358  abs00bd  11410  maxabslemlub  11551  xrmaxiflemcom  11593  xrmaxadd  11605  climconst  11634  isumz  11733  fsumf1o  11734  fsumcllem  11743  fsumadd  11750  fsumxp  11780  fsumcnv  11781  fsummulc2  11792  fsumconst  11798  fsumabs  11809  telfsumo  11810  fsumparts  11814  fsumrelem  11815  fsumiun  11821  binomlem  11827  binom  11828  binom11  11830  isumsplit  11835  arisum  11842  arisum2  11843  trireciplem  11844  georeclim  11857  cvgratnnlemseq  11870  prodfrecap  11890  prod1dc  11930  fprodf1o  11932  fprodcl2lem  11949  fprodcllem  11950  fprodfac  11959  fprod2d  11967  fprodxp  11968  fprodcnv  11969  fprodrec  11973  fprodmodd  11985  ef0lem  12004  ege2le3  12015  efaddlem  12018  efcan  12020  eft0val  12037  ef4p  12038  efgt1p2  12039  efi4p  12061  sincossq  12092  cos2tsin  12095  absefi  12113  demoivreALT  12118  p1modz1  12138  dvdsabseq  12191  odd2np1lem  12216  oddp1even  12220  opoe  12239  m1expo  12244  m1exp1  12245  nn0o1gt2  12249  bitsinv1  12306  gcddvds  12317  gcdcl  12320  gcdeq0  12331  gcd0id  12333  bezoutr1  12387  nnmindc  12388  nnminle  12389  eucalg  12414  lcm0val  12420  lcmid  12435  rpmul  12453  dfphi2  12575  phiprmpw  12577  hashgcdeq  12595  odzdvds  12601  nnnn0modprm0  12611  pythagtriplem4  12624  pythagtriplem12  12631  pcaddlem  12695  pcmpt  12699  pockthi  12714  4sqlem12  12758  2expltfac  12795  ennnfonelem0  12809  ennnfonelem1  12811  ennnfonelemhdmp1  12813  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemf1  12822  ctiunctlemfo  12843  setsresg  12903  strressid  12936  strle1g  12971  restid2  13113  prdsbas3  13152  gsumwmhm  13363  grplactcnv  13467  mulg0  13494  mulgnn0gsum  13497  mulgneg  13509  mulgneg2  13525  gsumfzconst  13710  gsumfzsnfd  13714  gsumfzfsumlem0  14381  zrhval2  14414  mpl0fi  14497  tgval2  14556  tgidm  14579  epttop  14595  tgrest  14674  restco  14679  restsn  14685  tgcn  14713  cnptopresti  14743  cnptoprest  14744  txbas  14763  upxp  14777  txrest  14781  txdis  14782  txhmeo  14824  txswaphmeolem  14825  xblss2ps  14909  xblss2  14910  qtopbasss  15026  fsumcncntop  15072  hoverb  15153  limcimolemlt  15169  dvcnp2cntop  15204  dvcoapbr  15212  dvexp  15216  dvexp2  15217  dvmptid  15221  dveflem  15231  dvef  15232  plymullem1  15253  plyadd  15256  plymul  15257  plycoeid3  15262  plycjlemc  15265  plycj  15266  sin0pilem1  15286  sin2kpi  15316  cos2kpi  15317  coseq0q4123  15339  coseq0negpitopi  15341  sincosq1eq  15344  sinkpi  15352  coskpi  15353  1cxp  15405  mpodvdsmulf1o  15495  lgslem2  15511  lgsfcl2  15516  lgs0  15523  lgs2  15527  lgsneg  15534  lgsdilem  15537  lgsdir2lem4  15541  lgsdir2lem5  15542  lgsne0  15548  lgssq  15550  lgssq2  15551  gausslemma2dlem3  15573  gausslemma2dlem4  15574  lgseisenlem1  15580  lgsquadlem2  15588  lgsquad2lem2  15592  lgsquad3  15594  m1lgs  15595  2lgslem1a2  15597  2lgsoddprmlem3  15621  2sqlem9  15634  2sqlem10  15635  edgiedgbg  15692  ex-ceil  15699  bj-intexr  15881  peano3nninf  15981  nninfall  15983  isomninnlem  16006  iswomni0  16027  ismkvnnlem  16028  nconstwlpolem0  16039