Theorem eqtr4d 2232

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 2202	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2229	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr2d  2235  3eqtr2rd  2236  3eqtr4d  2239  3eqtr4rd  2240  3eqtr4a  2255  sbnfc2  3145  ifsbdc  3574  ifeq1dadc  3592  ifeq2dadc  3593  eqifdc  3597  ifnotdc  3599  ifandc  3600  ifordc  3601  onsucuni2  4601  relop  4817  riinint  4928  iotauni  5232  fniinfv  5622  fsn2  5739  fmptapd  5756  fconst2g  5780  fniunfv  5812  ofres  6154  ofco  6158  caofid1  6168  caofid2  6169  frecsuclem  6473  frecrdg  6475  oasuc  6531  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  funresdfunsndc  6573  uniqs2  6663  en1bg  6868  fundmen  6874  1domsn  6887  pw2f1odclem  6904  mapxpen  6918  xpmapenlem  6919  phplem4dom  6932  en2eqpr  6977  sbthlemi5  7036  omp1eomlem  7169  difinfsnlem  7174  ctmlemr  7183  ctssdccl  7186  ctssdc  7188  infnninf  7199  infnninfOLD  7200  nnnninfeq  7203  exmidonfinlem  7274  exmidmotap  7346  addcmpblnq  7453  distrnqg  7473  ltexnqq  7494  addcmpblnq0  7529  nqnq0a  7540  nqnq0m  7541  nq0m0r  7542  nq0a0  7543  nnanq0  7544  distrnq0  7545  prarloclemlo  7580  prarloclemcalc  7588  genpassl  7610  genpassu  7611  ltsosr  7850  0idsr  7853  1idsr  7854  mulextsr1lem  7866  cnegex  8223  subsub3  8277  subadd4  8289  mulneg12  8442  mulsub  8446  apreap  8633  cru  8648  recextlem1  8697  cju  9007  ofnegsub  9008  halfaddsub  9244  nn0supp  9320  nneo  9448  zeo2  9451  uzin  9653  xaddcom  9955  xaddass  9963  xleaddadd  9981  iccf1o  10098  fzsuc2  10173  fldiv4lem1div2uz2  10415  flqeqceilz  10429  zmod1congr  10452  modqcyc  10470  modqcyc2  10471  modqaddabs  10473  modqmul1  10488  modqaddmulmod  10502  addmodlteq  10509  frec2uzrdg  10520  frecuzrdgsuctlem  10534  seq3val  10571  seqvalcd  10572  seq3fveq2  10586  seqfveq2g  10588  seq3split  10599  seqsplitg  10600  seqf1oglem2a  10629  seqf1oglem2  10631  seqfeq4g  10642  seq3distr  10643  ser0f  10645  expp1  10657  mulexp  10689  mulexpzap  10690  expadd  10692  expaddzap  10694  expmul  10695  expmulzap  10696  expsubap  10698  expdivap  10701  subsq  10757  mulbinom2  10767  binom3  10768  bernneq  10771  modqexp  10777  nn0opthd  10833  faclbnd  10852  faclbnd6  10855  bccmpl  10865  bcp1n  10872  zfz1isolemiso  10950  seq3coll  10953  shftval2  11010  shftval4  11012  seq3shft  11022  crre  11041  remim  11044  remullem  11055  cjexp  11077  cnrecnv  11094  resqrexlemlo  11197  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemcalc3  11200  resqrexlemnm  11202  rsqrmo  11211  abscj  11236  absid  11255  absre  11261  recvalap  11281  maxabsle  11388  maxltsup  11402  2zsupmax  11410  minabs  11420  bdtrilem  11423  bdtri  11424  2zinfmin  11427  xrmaxiflemab  11431  xrmaxiflemcom  11433  xrmaxadd  11445  xrbdtri  11460  iooinsup  11461  climaddc1  11513  climmulc2  11515  climsubc1  11516  climsubc2  11517  climcvg1nlem  11533  summodclem3  11564  zsumdc  11568  isum  11569  isumz  11573  isumss  11575  fisumss  11576  fsum3cvg2  11578  fsumadd  11590  isummulc2  11610  sumsplitdc  11616  fsum2dlemstep  11618  fisumcom2  11622  fisum0diag2  11631  fsumconst  11638  telfsumo  11650  fsumparts  11654  fsumrelem  11655  binomlem  11667  isumshft  11674  isumsplit  11675  arisum  11682  arisum2  11683  trireciplem  11684  geolim2  11696  geo2sum  11698  0.999...  11705  cvgratz  11716  mertensabs  11721  clim2prod  11723  prodf1f  11727  prodmodclem2a  11760  zproddc  11763  iprodap  11764  iprodap0  11766  fprodseq  11767  prod1dc  11770  prodssdc  11773  fprod2dlemstep  11806  fprodcom2fi  11810  fproddivap  11814  ef0lem  11844  efval2  11849  ege2le3  11855  efaddlem  11858  efsub  11865  eftlub  11874  efsep  11875  tanval3ap  11898  efi4p  11901  sinneg  11910  sinmul  11928  sincossq  11932  cos2t  11934  demoivreALT  11958  eirraplem  11961  dvdsmodexp  11979  odd2np1  12057  omoe  12080  divalglemex  12106  divalglemeuneg  12107  divalgmod  12111  flodddiv4  12120  bitsp1  12135  bitsinv1lem  12145  bitsinv1  12146  gcdneg  12176  gcdaddm  12178  modgcd  12185  bezoutlemnewy  12190  gcdass  12209  gcdmultiple  12214  nninfctlemfo  12234  algrp1  12241  lcmneg  12269  lcmgcdeq  12278  lcmass  12280  cncongr2  12299  prmexpb  12346  sqrt2irr  12357  2sqpwodd  12371  qnumdenbi  12387  phiprmpw  12417  eulerthlema  12425  fermltl  12429  prmdiveq  12431  modprm0  12450  pythagtriplem1  12461  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  pythagtriplem19  12478  pcpremul  12489  pcneg  12521  pcgcd  12525  pc2dvds  12526  pcaddlem  12535  pcprod  12542  fldivp1  12544  pcbc  12547  prmpwdvds  12551  pockthlem  12552  mul4sqlem  12589  4sqlem11  12597  4sqlem12  12598  4sqlem17  12603  ctiunctlemfo  12683  ressval3d  12777  resseqnbasd  12778  prdsval  12977  imasival  13010  qusval  13027  plusfeqg  13068  sgrp1  13115  idmhm  13173  resmhm2  13192  mhmeql  13196  grppropstrg  13223  grpinvinv  13271  grp1  13310  imasgrp2  13318  mulgnngsum  13335  mulginvcom  13355  mulgnndir  13359  mulgdir  13362  mulgneg2  13364  mulgnnass  13365  mulgass  13367  mulgsubdir  13370  trivsubgd  13408  nmzsubg  13418  qussub  13445  idghm  13467  ablinvadd  13518  ablsub2inv  13519  eqgabl  13538  mgpplusgg  13558  mgpbasg  13560  mgpscag  13561  mgptsetg  13562  mgpdsg  13564  mgpress  13565  srgpcomp  13624  srgpcompp  13625  ringo2times  13662  ring1eq0  13682  ring1  13693  opprmulfvalg  13704  crngoppr  13706  opprsllem  13708  oppr1g  13716  opprunitd  13744  rdivmuldivd  13778  rhmunitinv  13812  scafeqg  13942  lmodvsubval2  13976  lmodsubdi  13978  rmodislmod  13985  sralemg  14072  sraipg  14078  crng2idl  14165  cnfldmulg  14210  cnfldexp  14211  cnfldui  14223  mulgrhm2  14244  zrhrhmb  14256  zlmvscag  14267  znval2  14272  znbaslemnn  14273  znunit  14293  psrval  14300  psrgrp  14319  psrneg  14321  mplval2g  14329  restuni2  14521  lmfval  14536  cnfval  14538  cnpfval  14539  txtopon  14606  txcnp  14615  upxp  14616  txrest  14620  cnmptcom  14642  bl2in  14747  xblss2  14749  isxms2  14796  setsmsdsg  14824  setsmstsetg  14825  metss  14838  resubmet  14900  expcn  14913  cncfcncntop  14937  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvcoapbr  15051  dvcjbr  15052  dvexp  15055  dvexp2  15056  dvrecap  15057  plyaddlem1  15091  plymullem1  15092  plycolemc  15102  plycjlemc  15104  dvply1  15109  efimpi  15163  tangtx  15182  logdivlti  15225  cxpexprp  15239  rpcxpsub  15252  rpabscxpbnd  15284  rprelogbdiv  15301  binom4  15323  mpodvdsmulf1o  15334  0sgmppw  15337  lgslem1  15349  lgsmod  15375  lgsdilem  15376  lgsdi  15386  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  lgseisenlem2  15420  lgseisenlem3  15421  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  lgsquad3  15433  2lgslem3  15450  2lgsoddprmlem2  15455  2sqlem4  15467  bj-charfundcALT  15563  1dom1el  15745  2omap  15750  sssneq  15757  0nninf  15759  nnnninfex  15777  nninfnfiinf  15778  trilpolemisumle  15795