Theorem eqtr4d 2265

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 2235	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2262	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2d  2268  3eqtr2rd  2269  3eqtr4d  2272  3eqtr4rd  2273  3eqtr4a  2288  sbnfc2  3185  ifsbdc  3615  ifeq1dadc  3633  ifeq2dadc  3634  eqifdc  3639  ifnotdc  3641  2if2dc  3642  ifandc  3643  ifordc  3644  onsucuni2  4656  relop  4872  riinint  4985  iotauni  5291  fniinfv  5692  fsn2  5809  fmptapd  5830  fconst2g  5854  fniunfv  5886  ofres  6233  ofco  6237  caofid1  6247  caofid2  6248  frecsuclem  6552  frecrdg  6554  oasuc  6610  nnacom  6630  nnaass  6631  nndi  6632  nnmass  6633  nnmsucr  6634  nnmcom  6635  funresdfunsndc  6652  uniqs2  6742  en1bg  6952  fundmen  6959  1domsn  6976  pw2f1odclem  6995  mapxpen  7009  xpmapenlem  7010  phplem4dom  7023  en2eqpr  7069  sbthlemi5  7128  omp1eomlem  7261  difinfsnlem  7266  ctmlemr  7275  ctssdccl  7278  ctssdc  7280  infnninf  7291  infnninfOLD  7292  nnnninfeq  7295  pr2cv1  7368  exmidonfinlem  7371  exmidmotap  7447  addcmpblnq  7554  distrnqg  7574  ltexnqq  7595  addcmpblnq0  7630  nqnq0a  7641  nqnq0m  7642  nq0m0r  7643  nq0a0  7644  nnanq0  7645  distrnq0  7646  prarloclemlo  7681  prarloclemcalc  7689  genpassl  7711  genpassu  7712  ltsosr  7951  0idsr  7954  1idsr  7955  mulextsr1lem  7967  cnegex  8324  subsub3  8378  subadd4  8390  mulneg12  8543  mulsub  8547  apreap  8734  cru  8749  recextlem1  8798  cju  9108  ofnegsub  9109  halfaddsub  9345  nn0supp  9421  nneo  9550  zeo2  9553  uzin  9755  xaddcom  10057  xaddass  10065  xleaddadd  10083  iccf1o  10200  fzsuc2  10275  fldiv4lem1div2uz2  10526  flqeqceilz  10540  zmod1congr  10563  modqcyc  10581  modqcyc2  10582  modqaddabs  10584  modqmul1  10599  modqaddmulmod  10613  addmodlteq  10620  frec2uzrdg  10631  frecuzrdgsuctlem  10645  seq3val  10682  seqvalcd  10683  seq3fveq2  10697  seqfveq2g  10699  seq3split  10710  seqsplitg  10711  seqf1oglem2a  10740  seqf1oglem2  10742  seqfeq4g  10753  seq3distr  10754  ser0f  10756  expp1  10768  mulexp  10800  mulexpzap  10801  expadd  10803  expaddzap  10805  expmul  10806  expmulzap  10807  expsubap  10809  expdivap  10812  subsq  10868  mulbinom2  10878  binom3  10879  bernneq  10882  modqexp  10888  nn0opthd  10944  faclbnd  10963  faclbnd6  10966  bccmpl  10976  bcp1n  10983  zfz1isolemiso  11061  seq3coll  11064  ccatsymb  11137  ccatval1lsw  11139  ccatass  11143  eqs1  11161  lswccats1fst  11175  swrdsb0eq  11197  swrdsbslen  11198  swrds1  11200  ccatswrd  11202  pfxres  11213  ccatpfx  11233  pfxpfx  11240  cats1un  11253  swrdccatin1  11257  pfxccatin12  11265  swrdccat  11267  pfxccat3a  11270  swrdccat3b  11272  shftval2  11337  shftval4  11339  seq3shft  11349  crre  11368  remim  11371  remullem  11382  cjexp  11404  cnrecnv  11421  resqrexlemlo  11524  resqrexlemcalc1  11525  resqrexlemcalc2  11526  resqrexlemcalc3  11527  resqrexlemnm  11529  rsqrmo  11538  abscj  11563  absid  11582  absre  11588  recvalap  11608  maxabsle  11715  maxltsup  11729  2zsupmax  11737  minabs  11747  bdtrilem  11750  bdtri  11751  2zinfmin  11754  xrmaxiflemab  11758  xrmaxiflemcom  11760  xrmaxadd  11772  xrbdtri  11787  iooinsup  11788  climaddc1  11840  climmulc2  11842  climsubc1  11843  climsubc2  11844  climcvg1nlem  11860  summodclem3  11891  zsumdc  11895  isum  11896  isumz  11900  isumss  11902  fisumss  11903  fsum3cvg2  11905  fsumadd  11917  isummulc2  11937  sumsplitdc  11943  fsum2dlemstep  11945  fisumcom2  11949  fisum0diag2  11958  fsumconst  11965  telfsumo  11977  fsumparts  11981  fsumrelem  11982  binomlem  11994  isumshft  12001  isumsplit  12002  arisum  12009  arisum2  12010  trireciplem  12011  geolim2  12023  geo2sum  12025  0.999...  12032  cvgratz  12043  mertensabs  12048  clim2prod  12050  prodf1f  12054  prodmodclem2a  12087  zproddc  12090  iprodap  12091  iprodap0  12093  fprodseq  12094  prod1dc  12097  prodssdc  12100  fprod2dlemstep  12133  fprodcom2fi  12137  fproddivap  12141  ef0lem  12171  efval2  12176  ege2le3  12182  efaddlem  12185  efsub  12192  eftlub  12201  efsep  12202  tanval3ap  12225  efi4p  12228  sinneg  12237  sinmul  12255  sincossq  12259  cos2t  12261  demoivreALT  12285  eirraplem  12288  dvdsmodexp  12306  odd2np1  12384  omoe  12407  divalglemex  12433  divalglemeuneg  12434  divalgmod  12438  flodddiv4  12447  bitsp1  12462  bitsinv1lem  12472  bitsinv1  12473  gcdneg  12503  gcdaddm  12505  modgcd  12512  bezoutlemnewy  12517  gcdass  12536  gcdmultiple  12541  nninfctlemfo  12561  algrp1  12568  lcmneg  12596  lcmgcdeq  12605  lcmass  12607  cncongr2  12626  prmexpb  12673  sqrt2irr  12684  2sqpwodd  12698  qnumdenbi  12714  phiprmpw  12744  eulerthlema  12752  fermltl  12756  prmdiveq  12758  modprm0  12777  pythagtriplem1  12788  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem15  12801  pythagtriplem16  12802  pythagtriplem17  12803  pythagtriplem19  12805  pcpremul  12816  pcneg  12848  pcgcd  12852  pc2dvds  12853  pcaddlem  12862  pcprod  12869  fldivp1  12871  pcbc  12874  prmpwdvds  12878  pockthlem  12879  mul4sqlem  12916  4sqlem11  12924  4sqlem12  12925  4sqlem17  12930  ctiunctlemfo  13010  ressval3d  13105  resseqnbasd  13106  prdsval  13306  imasival  13339  qusval  13356  plusfeqg  13397  sgrp1  13444  idmhm  13502  resmhm2  13521  mhmeql  13525  grppropstrg  13552  grpinvinv  13600  grp1  13639  imasgrp2  13647  mulgnngsum  13664  mulginvcom  13684  mulgnndir  13688  mulgdir  13691  mulgneg2  13693  mulgnnass  13694  mulgass  13696  mulgsubdir  13699  trivsubgd  13737  nmzsubg  13747  qussub  13774  idghm  13796  ablinvadd  13847  ablsub2inv  13848  eqgabl  13867  mgpplusgg  13887  mgpbasg  13889  mgpscag  13890  mgptsetg  13891  mgpdsg  13893  mgpress  13894  srgpcomp  13953  srgpcompp  13954  ringo2times  13991  ring1eq0  14011  ring1  14022  opprmulfvalg  14033  crngoppr  14035  opprsllem  14037  oppr1g  14045  opprunitd  14074  rdivmuldivd  14108  rhmunitinv  14142  scafeqg  14272  lmodvsubval2  14306  lmodsubdi  14308  rmodislmod  14315  sralemg  14402  sraipg  14408  crng2idl  14495  cnfldmulg  14540  cnfldexp  14541  cnfldui  14553  mulgrhm2  14574  zrhrhmb  14586  zlmvscag  14597  znval2  14602  znbaslemnn  14603  znunit  14623  psrval  14630  psrgrp  14649  psrneg  14651  mplval2g  14659  restuni2  14851  lmfval  14867  cnfval  14868  cnpfval  14869  txtopon  14936  txcnp  14945  upxp  14946  txrest  14950  cnmptcom  14972  bl2in  15077  xblss2  15079  isxms2  15126  setsmsdsg  15154  setsmstsetg  15155  metss  15168  resubmet  15230  expcn  15243  cncfcncntop  15267  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvcoapbr  15381  dvcjbr  15382  dvexp  15385  dvexp2  15386  dvrecap  15387  plyaddlem1  15421  plymullem1  15422  plycolemc  15432  plycjlemc  15434  dvply1  15439  efimpi  15493  tangtx  15512  logdivlti  15555  cxpexprp  15569  rpcxpsub  15582  rpabscxpbnd  15614  rprelogbdiv  15631  binom4  15653  mpodvdsmulf1o  15664  0sgmppw  15667  lgslem1  15679  lgsmod  15705  lgsdilem  15706  lgsdi  15716  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  lgseisenlem2  15750  lgseisenlem3  15751  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem1  15760  lgsquad3  15763  2lgslem3  15780  2lgsoddprmlem2  15785  2sqlem4  15797  basvtxval2dom  15835  edgfiedgval2dom  15836  setsvtx  15852  ushgredgedgloop  16026  bj-charfundcALT  16172  1dom1el  16354  2omap  16359  sssneq  16368  0nninf  16370  nnnninfex  16388  nninfnfiinf  16389  trilpolemisumle  16406