Theorem eqtrdi 2219

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

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtr2di  2220  eqtr4di  2221  3eqtr3g  2226  3eqtr4a  2229  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  csbprc  3459  un00  3460  disjssun  3477  disjpr2  3645  tppreq3  3684  diftpsn3  3719  preq12b  3755  intsng  3863  uniintsnr  3865  rint0  3868  riin0  3942  iununir  3954  intexr  4134  sucprc  4395  op1stbg  4462  elreldm  4835  xpeq0r  5031  xpdisj1  5033  xpdisj2  5034  resdisj  5037  xpima1  5055  xpima2m  5056  elxp4  5096  unixp0im  5145  uniabio  5168  iotass  5175  cnvresid  5270  funimacnv  5272  f1o00  5475  dffv4g  5491  fnrnfv  5541  feqresmpt  5548  dffn5imf  5549  funfvdm2f  5559  fvun1  5560  fvmpt2  5577  fndmin  5600  fmptcof  5660  fmptcos  5661  fvunsng  5687  fvpr1  5697  fnrnov  5995  offval  6065  ofrfval  6066  op1std  6124  op2ndd  6125  fmpoco  6192  tpostpos  6240  tfr0  6299  rdgival  6358  frec0g  6373  2oconcl  6415  om0  6434  oei0  6435  oasuc  6440  omv2  6441  nnm0r  6455  uniqs2  6569  en1  6773  en1bg  6774  fundmen  6780  mapsnen  6785  xpsnen  6795  xpcomco  6800  xpdom2  6805  xpmapenlem  6823  exmidpweq  6883  unsnfidcex  6893  fiintim  6902  ssfirab  6907  sbthlemi8  6937  elfi2  6945  fi0  6948  fieq0  6949  djudom  7066  ismkvnex  7127  en2other2  7160  exmidfodomrlemim  7165  nq0m0r  7405  addpinq1  7413  genipv  7458  genpelvl  7461  genpelvu  7462  cauappcvgprlem1  7608  caucvgsrlemoffres  7749  addresr  7786  mulresr  7787  axcnre  7830  add20  8380  rimul  8491  rereim  8492  mulreim  8510  sup3exmid  8860  fv0p1e1  8980  div4p1lem1div2  9118  nnm1nn0  9163  znegcl  9230  peano2z  9235  nneoor  9301  nn0ind-raph  9316  xnegneg  9777  xltnegi  9779  xaddpnf1  9790  xnegid  9803  xnn0xadd0  9811  xnegdi  9812  xsubge0  9825  xposdif  9826  xlesubadd  9827  xleaddadd  9831  fz0to4untppr  10067  fzo0to2pr  10161  fldiv4p1lem1div2  10248  mulp1mod1  10308  frecfzennn  10369  iseqf1olemqk  10437  exp0  10467  expp1  10470  expnegap0  10471  1exp  10492  mulexp  10502  m1expeven  10510  sq0i  10554  bernneq  10583  facp1  10651  faclbnd3  10664  facubnd  10666  bcval5  10684  hashinfom  10699  hashsng  10720  hashxp  10748  resunimafz0  10753  zfz1iso  10763  imre  10802  reim0b  10813  rereb  10814  resqrexlemover  10961  resqrexlemcalc1  10965  abs00bd  11017  maxabslemlub  11158  xrmaxiflemcom  11199  xrmaxadd  11211  climconst  11240  isumz  11339  fsumf1o  11340  fsumcllem  11349  fsumadd  11356  fsumxp  11386  fsumcnv  11387  fsummulc2  11398  fsumconst  11404  fsumabs  11415  telfsumo  11416  fsumparts  11420  fsumrelem  11421  fsumiun  11427  binomlem  11433  binom  11434  binom11  11436  isumsplit  11441  arisum  11448  arisum2  11449  trireciplem  11450  georeclim  11463  cvgratnnlemseq  11476  prodfrecap  11496  prod1dc  11536  fprodf1o  11538  fprodcl2lem  11555  fprodcllem  11556  fprodfac  11565  fprod2d  11573  fprodxp  11574  fprodcnv  11575  fprodrec  11579  fprodmodd  11591  ef0lem  11610  ege2le3  11621  efaddlem  11624  efcan  11626  eft0val  11643  ef4p  11644  efgt1p2  11645  efi4p  11667  sincossq  11698  cos2tsin  11701  absefi  11718  demoivreALT  11723  p1modz1  11743  dvdsabseq  11794  odd2np1lem  11818  oddp1even  11822  opoe  11841  m1expo  11846  m1exp1  11847  nn0o1gt2  11851  nninfdcex  11895  gcddvds  11905  gcdcl  11908  gcdeq0  11919  gcd0id  11921  bezoutr1  11975  nnmindc  11976  nnminle  11977  eucalg  12000  lcm0val  12006  lcmid  12021  rpmul  12039  dfphi2  12161  phiprmpw  12163  hashgcdeq  12180  odzdvds  12186  nnnn0modprm0  12196  pythagtriplem4  12209  pythagtriplem12  12216  pcaddlem  12279  pcmpt  12282  pockthi  12297  ennnfonelem0  12347  ennnfonelem1  12349  ennnfonelemhdmp1  12351  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemf1  12360  ctiunctlemfo  12381  setsresg  12441  strle1g  12495  restid2  12575  tgval2  12804  tgidm  12827  epttop  12843  tgrest  12922  restco  12927  restsn  12933  tgcn  12961  cnptopresti  12991  cnptoprest  12992  txbas  13011  upxp  13025  txrest  13029  txdis  13030  txhmeo  13072  txswaphmeolem  13073  xblss2ps  13157  xblss2  13158  qtopbasss  13274  fsumcncntop  13309  limcimolemlt  13386  dvcnp2cntop  13416  dvcoapbr  13424  dvexp  13428  dvexp2  13429  dveflem  13440  dvef  13441  sin0pilem1  13455  sin2kpi  13485  cos2kpi  13486  coseq0q4123  13508  coseq0negpitopi  13510  sincosq1eq  13513  sinkpi  13521  coskpi  13522  1cxp  13574  lgslem2  13655  lgsfcl2  13660  lgs0  13667  lgs2  13671  lgsneg  13678  lgsdilem  13681  lgsdir2lem4  13685  lgsdir2lem5  13686  lgsne0  13692  lgssq  13694  lgssq2  13695  2sqlem9  13713  2sqlem10  13714  ex-ceil  13720  bj-intexr  13903  exmid1stab  13993  peano3nninf  14000  nninfall  14002  isomninnlem  14022  iswomni0  14043  ismkvnnlem  14044  nconstwlpolem0  14054