Theorem eqtr4d 2267

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

Hypotheses

Ref	Expression
eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4d	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2264	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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:  3eqtr2d  2270  3eqtr2rd  2271  3eqtr4d  2274  3eqtr4rd  2275  3eqtr4a  2290  sbnfc2  3188  ifsbdc  3618  ifeq1dadc  3636  ifeq2dadc  3637  eqifdc  3642  ifnotdc  3644  2if2dc  3645  ifandc  3646  ifordc  3647  onsucuni2  4662  relop  4880  riinint  4993  iotauni  5299  fniinfv  5704  fsn2  5821  fmptapd  5844  fconst2g  5868  fniunfv  5902  ofres  6249  ofco  6253  caofid1  6263  caofid2  6264  frecsuclem  6571  frecrdg  6573  oasuc  6631  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  funresdfunsndc  6673  uniqs2  6763  en1bg  6973  fundmen  6980  1dom1el  6992  1domsn  7000  pw2f1odclem  7019  mapxpen  7033  xpmapenlem  7034  phplem4dom  7047  en2eqpr  7098  sbthlemi5  7159  omp1eomlem  7292  difinfsnlem  7297  ctmlemr  7306  ctssdccl  7309  ctssdc  7311  infnninf  7322  infnninfOLD  7323  nnnninfeq  7326  pr2cv1  7399  exmidonfinlem  7403  exmidmotap  7479  addcmpblnq  7586  distrnqg  7606  ltexnqq  7627  addcmpblnq0  7662  nqnq0a  7673  nqnq0m  7674  nq0m0r  7675  nq0a0  7676  nnanq0  7677  distrnq0  7678  prarloclemlo  7713  prarloclemcalc  7721  genpassl  7743  genpassu  7744  ltsosr  7983  0idsr  7986  1idsr  7987  mulextsr1lem  7999  cnegex  8356  subsub3  8410  subadd4  8422  mulneg12  8575  mulsub  8579  apreap  8766  cru  8781  recextlem1  8830  cju  9140  ofnegsub  9141  halfaddsub  9377  nn0supp  9453  nneo  9582  zeo2  9585  uzin  9788  xaddcom  10095  xaddass  10103  xleaddadd  10121  iccf1o  10238  fzsuc2  10313  fldiv4lem1div2uz2  10565  flqeqceilz  10579  zmod1congr  10602  modqcyc  10620  modqcyc2  10621  modqaddabs  10623  modqmul1  10638  modqaddmulmod  10652  addmodlteq  10659  frec2uzrdg  10670  frecuzrdgsuctlem  10684  seq3val  10721  seqvalcd  10722  seq3fveq2  10736  seqfveq2g  10738  seq3split  10749  seqsplitg  10750  seqf1oglem2a  10779  seqf1oglem2  10781  seqfeq4g  10792  seq3distr  10793  ser0f  10795  expp1  10807  mulexp  10839  mulexpzap  10840  expadd  10842  expaddzap  10844  expmul  10845  expmulzap  10846  expsubap  10848  expdivap  10851  subsq  10907  mulbinom2  10917  binom3  10918  bernneq  10921  modqexp  10927  nn0opthd  10983  faclbnd  11002  faclbnd6  11005  bccmpl  11015  bcp1n  11022  zfz1isolemiso  11102  seq3coll  11105  ccatsymb  11178  ccatval1lsw  11180  ccatass  11184  eqs1  11204  lswccats1fst  11220  swrdsb0eq  11245  swrdsbslen  11246  swrds1  11248  ccatswrd  11250  pfxres  11261  ccatpfx  11281  pfxpfx  11288  cats1un  11301  swrdccatin1  11305  pfxccatin12  11313  swrdccat  11315  pfxccat3a  11318  swrdccat3b  11320  shftval2  11386  shftval4  11388  seq3shft  11398  crre  11417  remim  11420  remullem  11431  cjexp  11453  cnrecnv  11470  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnm  11578  rsqrmo  11587  abscj  11612  absid  11631  absre  11637  recvalap  11657  maxabsle  11764  maxltsup  11778  2zsupmax  11786  minabs  11796  bdtrilem  11799  bdtri  11800  2zinfmin  11803  xrmaxiflemab  11807  xrmaxiflemcom  11809  xrmaxadd  11821  xrbdtri  11836  iooinsup  11837  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  climcvg1nlem  11909  summodclem3  11940  zsumdc  11944  isum  11945  isumz  11949  isumss  11951  fisumss  11952  fsum3cvg2  11954  fsumadd  11966  isummulc2  11986  sumsplitdc  11992  fsum2dlemstep  11994  fisumcom2  11998  fisum0diag2  12007  fsumconst  12014  telfsumo  12026  fsumparts  12030  fsumrelem  12031  binomlem  12043  isumshft  12050  isumsplit  12051  arisum  12058  arisum2  12059  trireciplem  12060  geolim2  12072  geo2sum  12074  0.999...  12081  cvgratz  12092  mertensabs  12097  clim2prod  12099  prodf1f  12103  prodmodclem2a  12136  zproddc  12139  iprodap  12140  iprodap0  12142  fprodseq  12143  prod1dc  12146  prodssdc  12149  fprod2dlemstep  12182  fprodcom2fi  12186  fproddivap  12190  ef0lem  12220  efval2  12225  ege2le3  12231  efaddlem  12234  efsub  12241  eftlub  12250  efsep  12251  tanval3ap  12274  efi4p  12277  sinneg  12286  sinmul  12304  sincossq  12308  cos2t  12310  demoivreALT  12334  eirraplem  12337  dvdsmodexp  12355  odd2np1  12433  omoe  12456  divalglemex  12482  divalglemeuneg  12483  divalgmod  12487  flodddiv4  12496  bitsp1  12511  bitsinv1lem  12521  bitsinv1  12522  gcdneg  12552  gcdaddm  12554  modgcd  12561  bezoutlemnewy  12566  gcdass  12585  gcdmultiple  12590  nninfctlemfo  12610  algrp1  12617  lcmneg  12645  lcmgcdeq  12654  lcmass  12656  cncongr2  12675  prmexpb  12722  sqrt2irr  12733  2sqpwodd  12747  qnumdenbi  12763  phiprmpw  12793  eulerthlema  12801  fermltl  12805  prmdiveq  12807  modprm0  12826  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  pythagtriplem19  12854  pcpremul  12865  pcneg  12897  pcgcd  12901  pc2dvds  12902  pcaddlem  12911  pcprod  12918  fldivp1  12920  pcbc  12923  prmpwdvds  12927  pockthlem  12928  mul4sqlem  12965  4sqlem11  12973  4sqlem12  12974  4sqlem17  12979  ctiunctlemfo  13059  ressval3d  13154  resseqnbasd  13155  prdsval  13355  imasival  13388  qusval  13405  plusfeqg  13446  sgrp1  13493  idmhm  13551  resmhm2  13570  mhmeql  13574  grppropstrg  13601  grpinvinv  13649  grp1  13688  imasgrp2  13696  mulgnngsum  13713  mulginvcom  13733  mulgnndir  13737  mulgdir  13740  mulgneg2  13742  mulgnnass  13743  mulgass  13745  mulgsubdir  13748  trivsubgd  13786  nmzsubg  13796  qussub  13823  idghm  13845  ablinvadd  13896  ablsub2inv  13897  eqgabl  13916  mgpplusgg  13936  mgpbasg  13938  mgpscag  13939  mgptsetg  13940  mgpdsg  13942  mgpress  13943  srgpcomp  14002  srgpcompp  14003  ringo2times  14040  ring1eq0  14060  ring1  14071  opprmulfvalg  14082  crngoppr  14084  opprsllem  14086  oppr1g  14094  opprunitd  14123  rdivmuldivd  14157  rhmunitinv  14191  scafeqg  14321  lmodvsubval2  14355  lmodsubdi  14357  rmodislmod  14364  sralemg  14451  sraipg  14457  crng2idl  14544  cnfldmulg  14589  cnfldexp  14590  cnfldui  14602  mulgrhm2  14623  zrhrhmb  14635  zlmvscag  14646  znval2  14651  znbaslemnn  14652  znunit  14672  psrval  14679  psrgrp  14698  psrneg  14700  mplval2g  14708  restuni2  14900  lmfval  14916  cnfval  14917  cnpfval  14918  txtopon  14985  txcnp  14994  upxp  14995  txrest  14999  cnmptcom  15021  bl2in  15126  xblss2  15128  isxms2  15175  setsmsdsg  15203  setsmstsetg  15204  metss  15217  resubmet  15279  expcn  15292  cncfcncntop  15316  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvcoapbr  15430  dvcjbr  15431  dvexp  15434  dvexp2  15435  dvrecap  15436  plyaddlem1  15470  plymullem1  15471  plycolemc  15481  plycjlemc  15483  dvply1  15488  efimpi  15542  tangtx  15561  logdivlti  15604  cxpexprp  15618  rpcxpsub  15631  rpabscxpbnd  15663  rprelogbdiv  15680  binom4  15702  mpodvdsmulf1o  15713  0sgmppw  15716  lgslem1  15728  lgsmod  15754  lgsdilem  15755  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  lgsquad3  15812  2lgslem3  15829  2lgsoddprmlem2  15834  2sqlem4  15846  basvtxval2dom  15884  edgfiedgval2dom  15885  setsvtx  15901  ushgredgedgloop  16078  usgr1vr  16098  wlkres  16229  clwwlkccatlem  16250  bj-charfundcALT  16404  pw1ndom3lem  16588  pw1ndom3  16589  2omap  16594  sssneq  16603  0nninf  16606  nnnninfex  16624  nninfnfiinf  16625  trilpolemisumle  16642  gsumgfsum  16684