Theorem eqtrdi 2280

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtr2di  2281  eqtr4di  2282  3eqtr3g  2287  3eqtr4a  2290  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  csbprc  3540  un00  3541  disjssun  3558  disjpr2  3733  tppreq3  3774  diftpsn3  3814  ssprsseq  3835  preq12b  3853  intsng  3962  uniintsnr  3964  rint0  3967  riin0  4042  iununir  4054  intexr  4240  exmid1stab  4298  sucprc  4509  op1stbg  4576  elreldm  4958  xpeq0r  5159  xpdisj1  5161  xpdisj2  5162  resdisj  5165  xpima1  5183  xpima2m  5184  elxp4  5224  unixp0im  5273  uniabio  5297  iotass  5304  cnvresid  5404  funimacnv  5406  fimadmfo  5568  f1o00  5620  dffv4g  5636  fv2prc  5678  fnrnfv  5692  feqresmpt  5700  dffn5imf  5701  funfvdm2f  5711  fvun1  5712  fvmpt2  5730  fndmin  5754  fmptcof  5814  fmptcos  5815  funopdmsn  5834  fvunsng  5848  fvpr1  5858  fnrnov  6168  offval  6243  ofrfval  6244  op1std  6311  op2ndd  6312  fmpoco  6381  tpostpos  6430  tfr0  6489  rdgival  6548  frec0g  6563  2oconcl  6607  om0  6626  oei0  6627  oasuc  6632  omv2  6633  nnm0r  6647  uniqs2  6764  en1  6973  en1bg  6974  fundmen  6981  mapsnen  6986  en2  6998  xpsnen  7005  xpcomco  7010  xpdom2  7015  xpmapenlem  7035  exmidpweq  7101  unsnfidcex  7112  fiintim  7123  ssfirab  7129  sbthlemi8  7163  elfi2  7171  fi0  7174  fieq0  7175  djudom  7292  ismkvnex  7354  nninfwlpoimlemg  7374  en2other2  7407  exmidfodomrlemim  7412  nq0m0r  7676  addpinq1  7684  genipv  7729  genpelvl  7732  genpelvu  7733  cauappcvgprlem1  7879  caucvgsrlemoffres  8020  addresr  8057  mulresr  8058  axcnre  8101  add20  8654  rimul  8765  rereim  8766  mulreim  8784  sup3exmid  9137  fv0p1e1  9258  div4p1lem1div2  9398  nnm1nn0  9443  znegcl  9510  peano2z  9515  nneoor  9582  nn0ind-raph  9597  xnegneg  10068  xltnegi  10070  xaddpnf1  10081  xnegid  10094  xnn0xadd0  10102  xnegdi  10103  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  fz0to4untppr  10359  fzo0to2pr  10464  nninfdcex  10498  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  mulp1mod1  10628  frecfzennn  10689  iseqf1olemqk  10770  exp0  10806  expp1  10809  expnegap0  10810  1exp  10831  mulexp  10841  m1expeven  10849  sq0i  10894  bernneq  10923  facp1  10993  faclbnd3  11006  facubnd  11008  bcval5  11026  hashinfom  11041  hashsng  11061  hashxp  11091  resunimafz0  11096  zfz1iso  11106  hash2en  11108  lsw1  11164  s1rn  11196  eqs1  11206  ccat1st1st  11219  swrd00g  11231  swrdlend  11240  swrds1  11250  cats1lend  11349  cats2catd  11351  s2leng  11371  s2dmg  11372  imre  11413  reim0b  11424  rereb  11425  resqrexlemover  11572  resqrexlemcalc1  11576  abs00bd  11628  maxabslemlub  11769  xrmaxiflemcom  11811  xrmaxadd  11823  climconst  11852  fzf1o  11938  isumz  11952  fsumf1o  11953  fsumcllem  11962  fsumadd  11969  fsumxp  11999  fsumcnv  12000  fsummulc2  12011  fsumconst  12017  fsumabs  12028  telfsumo  12029  fsumparts  12033  fsumrelem  12034  fsumiun  12040  binomlem  12046  binom  12047  binom11  12049  isumsplit  12054  arisum  12061  arisum2  12062  trireciplem  12063  georeclim  12076  cvgratnnlemseq  12089  prodfrecap  12109  prod1dc  12149  fprodf1o  12151  fprodcl2lem  12168  fprodcllem  12169  fprodfac  12178  fprod2d  12186  fprodxp  12187  fprodcnv  12188  fprodrec  12192  fprodmodd  12204  ef0lem  12223  ege2le3  12234  efaddlem  12237  efcan  12239  eft0val  12256  ef4p  12257  efgt1p2  12258  efi4p  12280  sincossq  12311  cos2tsin  12314  absefi  12332  demoivreALT  12337  p1modz1  12357  dvdsabseq  12410  odd2np1lem  12435  oddp1even  12439  opoe  12458  m1expo  12463  m1exp1  12464  nn0o1gt2  12468  bitsinv1  12525  gcddvds  12536  gcdcl  12539  gcdeq0  12550  gcd0id  12552  bezoutr1  12606  nnmindc  12607  nnminle  12608  eucalg  12633  lcm0val  12639  lcmid  12654  rpmul  12672  dfphi2  12794  phiprmpw  12796  hashgcdeq  12814  odzdvds  12820  nnnn0modprm0  12830  pythagtriplem4  12843  pythagtriplem12  12850  pcaddlem  12914  pcmpt  12918  pockthi  12933  4sqlem12  12977  2expltfac  13014  ennnfonelem0  13028  ennnfonelem1  13030  ennnfonelemhdmp1  13032  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemf1  13041  ctiunctlemfo  13062  setsresg  13122  strressid  13156  strle1g  13191  restid2  13333  prdsbas3  13372  gsumwmhm  13583  grplactcnv  13687  mulg0  13714  mulgnn0gsum  13717  mulgneg  13729  mulgneg2  13745  gsumfzconst  13930  gsumfzsnfd  13934  gsumsplit0  13935  gsumfzfsumlem0  14603  zrhval2  14636  mpl0fi  14719  tgval2  14778  tgidm  14801  epttop  14817  tgrest  14896  restco  14901  restsn  14907  tgcn  14935  cnptopresti  14965  cnptoprest  14966  txbas  14985  upxp  14999  txrest  15003  txdis  15004  txhmeo  15046  txswaphmeolem  15047  xblss2ps  15131  xblss2  15132  qtopbasss  15248  fsumcncntop  15294  hoverb  15375  limcimolemlt  15391  dvcnp2cntop  15426  dvcoapbr  15434  dvexp  15438  dvexp2  15439  dvmptid  15443  dveflem  15453  dvef  15454  plymullem1  15475  plyadd  15478  plymul  15479  plycoeid3  15484  plycjlemc  15487  plycj  15488  sin0pilem1  15508  sin2kpi  15538  cos2kpi  15539  coseq0q4123  15561  coseq0negpitopi  15563  sincosq1eq  15566  sinkpi  15574  coskpi  15575  1cxp  15627  mpodvdsmulf1o  15717  lgslem2  15733  lgsfcl2  15738  lgs0  15745  lgs2  15749  lgsneg  15756  lgsdilem  15759  lgsdir2lem4  15763  lgsdir2lem5  15764  lgsne0  15770  lgssq  15772  lgssq2  15773  gausslemma2dlem3  15795  gausslemma2dlem4  15796  lgseisenlem1  15802  lgsquadlem2  15810  lgsquad2lem2  15814  lgsquad3  15816  m1lgs  15817  2lgslem1a2  15819  2lgsoddprmlem3  15843  2sqlem9  15856  2sqlem10  15857  edgiedgbg  15919  isuhgrm  15925  isushgrm  15926  uhgr0vb  15938  uhgrun  15940  isupgren  15949  isumgren  15959  umgrnloop0  15971  upgrun  15980  umgrun  15982  isuspgren  16011  isusgren  16012  usgrf1oedg  16059  usgredg3  16068  egrsubgr  16117  0uhgrsubgr  16119  uhgrspansubgrlem  16130  vtxdg0v  16148  vtxdgfi0e  16149  vtxdfifiun  16151  vtxdumgrfival  16152  1loopgrvd2fi  16159  vdegp1cid  16170  wlkl1loop  16212  2wlklem  16230  upgr2wlkdc  16231  clwwlkn0  16262  clwwlkn1  16272  clwwlkn2  16275  umgr2cwwk2dif  16278  clwwlk0on0  16285  clwwlknonel  16286  clwwlknonex2lem1  16291  trlsegvdeglem4  16317  eupthvdres  16329  eupth2lembfi  16331  ex-ceil  16339  bj-intexr  16524  peano3nninf  16630  nninfall  16632  isomninnlem  16655  iswomni0  16676  ismkvnnlem  16677  nconstwlpolem0  16688  gfsumval  16701  gfsumsn  16706  gfsump1  16707