Theorem eqtr4d 2274

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- ( ph -> A = B )
2		eqtr4d.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2244	. 2 |- ( ph -> B = C )
4	1, 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:  3eqtr2d  2277  3eqtr2rd  2278  3eqtr4d  2281  3eqtr4rd  2282  3eqtr4a  2297  sbnfc2  3208  ifsbdc  3653  ifeq1dadc  3671  ifeq2dadc  3672  eqifdc  3677  ifnotdc  3679  2if2dc  3680  ifandc  3681  ifordc  3682  ifeqeqxdc  3687  onsucuni2  4711  relop  4930  riinint  5043  iotauni  5350  fniinfv  5761  fsn2  5882  fmptapd  5906  fconst2g  5930  fniunfv  5968  ofres  6317  ofco  6321  caofid1  6331  caofid2  6332  fsuppeq  6487  fsuppeqg  6488  frecsuclem  6677  frecrdg  6679  oasuc  6737  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  funresdfunsndc  6779  uniqs2  6869  en1bg  7087  fundmen  7094  1dom1el  7107  1domsn  7115  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  mapunen  7151  phplem4dom  7163  en2eqpr  7214  sbthlemi5  7278  2omap  7319  omp1eomlem  7435  difinfsnlem  7440  ctmlemr  7449  ctssdccl  7452  ctssdc  7454  infnninf  7465  infnninfOLD  7466  nnnninfeq  7469  pr2cv1  7542  exmidonfinlem  7546  exmidmotap  7628  addcmpblnq  7735  distrnqg  7755  ltexnqq  7776  addcmpblnq0  7811  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  nq0a0  7825  nnanq0  7826  distrnq0  7827  prarloclemlo  7862  prarloclemcalc  7870  genpassl  7892  genpassu  7893  ltsosr  8132  0idsr  8135  1idsr  8136  mulextsr1lem  8148  cnegex  8506  subsub3  8560  subadd4  8572  mulneg12  8726  mulsub  8730  apreap  8918  cru  8933  recextlem1  8982  cju  9294  ofnegsub  9295  halfaddsub  9544  nn0supp  9624  nneo  9754  zeo2  9757  uzin  9965  xaddcom  10274  xaddass  10282  xleaddadd  10300  iccf1o  10418  fzsuc2  10497  fldiv4lem1div2uz2  10756  flqeqceilz  10770  zmod1congr  10793  modqcyc  10811  modqcyc2  10812  modqaddabs  10814  modqmul1  10829  modqaddmulmod  10843  addmodlteq  10850  frec2uzrdg  10861  frecuzrdgsuctlem  10875  seq3val  10912  seqvalcd  10913  seq3fveq2  10927  seqfveq2g  10929  seq3split  10940  seqsplitg  10941  seqf1oglem2a  10970  seqf1oglem2  10972  seqfeq4g  10983  seq3distr  10984  ser0f  10986  expp1  10998  mulexp  11030  mulexpzap  11031  expadd  11033  expaddzap  11035  expmul  11036  expmulzap  11037  expsubap  11039  expdivap  11042  subsq  11098  mulbinom2  11108  binom3  11109  bernneq  11113  modqexp  11119  nn0opthd  11176  faclbnd  11195  faclbnd6  11198  bccmpl  11208  bcp1n  11215  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1  11303  zfz1isolemiso  11307  seq3coll  11310  hashtpglem  11314  ccatsymb  11386  ccatval1lsw  11388  ccatass  11392  eqs1  11412  lswccats1fst  11428  swrdsb0eq  11453  swrdsbslen  11454  swrds1  11456  ccatswrd  11458  pfxres  11469  ccatpfx  11489  pfxpfx  11496  cats1un  11509  swrdccatin1  11513  pfxccatin12  11521  swrdccat  11523  pfxccat3a  11526  swrdccat3b  11528  shftval2  11607  shftval4  11609  seq3shft  11619  crre  11638  remim  11641  remullem  11652  cjexp  11674  sq01  11676  cnrecnv  11692  resqrexlemlo  11795  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnm  11800  rsqrmo  11809  abscj  11834  absid  11853  absre  11860  recvalap  11880  maxabsle  11987  maxltsup  12001  2zsupmax  12009  minabs  12020  bdtrilem  12024  bdtri  12025  2zinfmin  12028  xrmaxiflemab  12032  xrmaxiflemcom  12034  xrmaxadd  12046  xrbdtri  12061  iooinsup  12062  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climcvg1nlem  12134  summodclem3  12166  zsumdc  12170  isum  12171  isumz  12175  isumss  12177  fisumss  12178  fsum3cvg2  12180  fsumadd  12192  isummulc2  12212  sumsplitdc  12218  fsum2dlemstep  12220  fisumcom2  12224  fisum0diag2  12233  fsumconst  12240  telfsumo  12252  fsumparts  12256  fsumrelem  12257  binomlem  12269  isumshft  12276  isumsplit  12277  arisum  12284  arisum2  12285  trireciplem  12286  geolim2  12298  geo2sum  12300  0.999...  12307  cvgratz  12318  mertensabs  12323  clim2prod  12325  prodf1f  12329  prodmodclem2a  12362  zproddc  12365  iprodap  12366  iprodap0  12368  fprodseq  12369  prod1dc  12372  prodssdc  12375  fprod2dlemstep  12408  fprodcom2fi  12412  fproddivap  12416  ef0lem  12446  efval2  12451  ege2le3  12457  efaddlem  12460  efsub  12467  eftlub  12476  efsep  12477  tanval3ap  12500  efi4p  12503  sinneg  12512  sinmul  12530  sincossq  12534  cos2t  12536  demoivreALT  12560  eirraplem  12563  dvdsmodexp  12581  odd2np1  12659  omoe  12682  divalglemex  12708  divalglemeuneg  12709  divalgmod  12713  flodddiv4  12722  bitsp1  12737  bitsinv1lem  12747  bitsinv1  12748  gcdneg  12778  gcdaddm  12780  modgcd  12787  bezoutlemnewy  12792  gcdass  12811  gcdmultiple  12816  nninfctlemfo  12836  algrp1  12843  lcmneg  12871  lcmgcdeq  12880  lcmass  12882  cncongr2  12901  prmexpb  12949  sqrt2irr  12960  2sqpwodd  12975  qnumdenbi  12991  nn0sqdcq  13007  sqrtrirr  13008  phiprmpw  13023  eulerthlema  13031  fermltl  13035  prmdiveq  13037  modprm0  13056  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem19  13084  pcpremul  13095  pcneg  13127  pcgcd  13131  pc2dvds  13132  pcaddlem  13141  pcprod  13148  fldivp1  13150  pcbc  13153  prmpwdvds  13157  pockthlem  13158  mul4sqlem  13195  4sqlem11  13203  4sqlem12  13204  4sqlem17  13209  ballotfilemrv  13315  ballotfilemfg  13321  ballotfilemfrc  13322  ballotfilemrinv0  13328  ctiunctlemfo  13382  ressval3d  13479  resseqnbasd  13480  imasival  13680  qusval  13697  plusfeqg  13737  sgrp1  13779  idmhm  13829  resmhm2  13848  mhmeql  13852  grppropstrg  13877  grpinvinv  13925  grp1  13964  imasgrp2  13966  mulgnngzsum  13983  mulginvcom  14003  mulgnndir  14007  mulgdir  14010  mulgneg2  14012  mulgnnass  14013  mulgass  14015  mulgsubdir  14018  trivsubgd  14056  nmzsubg  14066  qussub  14093  idghm  14115  cntzsubm  14164  cntzsubg  14165  ablinvadd  14198  ablsub2inv  14199  eqgabl  14218  gzsumgsum  14239  gsump1  14241  gsumconstcmn  14250  prdsval  14257  mgpplusgg  14305  mgpbasg  14308  mgpscag  14310  mgptsetg  14311  mgpdsg  14313  mgpress  14314  srgpcomp  14378  srgpcompp  14379  ringo2times  14417  ring1eq0  14437  ring1  14448  opprmulfvalg  14459  crngoppr  14461  opprsllem  14463  oppr1g  14472  opprunitd  14501  rdivmuldivd  14535  rhmunitinv  14569  scafeqg  14729  lmodvsubval2  14763  lmodsubdi  14765  rmodislmod  14772  sralemg  14859  sraipg  14865  crng2idl  14952  cnfldmulg  14997  cnfldexp  14998  cnfldui  15008  mulgrhm2  15029  zrhrhmb  15041  zlmvscag  15052  znval2  15057  znbaslemnn  15058  znunit  15078  psrval  15134  psrmulrg  15158  psrgrp  15167  psrneg  15169  mplval2g  15177  restuni2  15369  lmfval  15385  cnfval  15386  cnpfval  15387  txtopon  15454  txcnp  15463  upxp  15464  txrest  15468  cnmptcom  15490  bl2in  15595  xblss2  15597  isxms2  15644  setsmsdsg  15672  setsmstsetg  15673  metss  15686  resubmet  15748  expcn  15761  cncfcncntop  15785  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvcoapbr  15899  dvcjbr  15900  dvexp  15903  dvexp2  15904  dvrecap  15905  plyaddlem1  15939  plymullem1  15940  plycolemc  15950  plycjlemc  15952  dvply1  15957  efimpi  16012  tangtx  16031  logdivlti  16075  logfac  16090  cxpexprp  16092  rpcxpsub  16105  rpabscxpbnd  16137  rprelogbdiv  16154  binom4  16180  log2tlbndlog2  16181  birthdaylem2  16187  pellexlem2  16191  prmorcht  16243  mpodvdsmulf1o  16245  0sgmppw  16248  chtqleppi  16255  chtublem  16256  pcbcctr  16264  bcmono  16265  bcp1ctr  16267  bclbnd  16268  bposlem3  16274  bposlem9  16280  lgslem1  16285  lgsmod  16311  lgsdilem  16312  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem1  16366  lgsquad3  16369  2lgslem3  16386  2lgsoddprmlem2  16391  2sqlem4  16403  basvtxval2dom  16441  edgfiedgval2dom  16442  setsvtx  16458  ushgredgedgloop  16635  usgr1vr  16655  wlkres  16786  clwwlkccatlem  16807  trlsegvdegfi  16874  eupth2lem3lem2fi  16876  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  depindlem3  16915  bj-charfundcALT  17001  pw1ndom3lem  17185  pw1ndom3  17186  sssneq  17198  0nninf  17213  nnnninfex  17231  nninfnfiinf  17232  repiecele0  17241  trilpolemisumle  17254  qdiff  17265