Theorem eqtr4d 2229

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 2199	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2226	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr2d  2232  3eqtr2rd  2233  3eqtr4d  2236  3eqtr4rd  2237  3eqtr4a  2252  sbnfc2  3141  ifsbdc  3569  ifeq1dadc  3587  ifeq2dadc  3588  eqifdc  3592  ifnotdc  3594  ifandc  3595  ifordc  3596  onsucuni2  4596  relop  4812  riinint  4923  iotauni  5227  fniinfv  5615  fsn2  5732  fmptapd  5749  fconst2g  5773  fniunfv  5805  ofres  6145  ofco  6149  frecsuclem  6459  frecrdg  6461  oasuc  6517  nnacom  6537  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  funresdfunsndc  6559  uniqs2  6649  en1bg  6854  fundmen  6860  1domsn  6873  pw2f1odclem  6890  mapxpen  6904  xpmapenlem  6905  phplem4dom  6918  en2eqpr  6963  sbthlemi5  7020  omp1eomlem  7153  difinfsnlem  7158  ctmlemr  7167  ctssdccl  7170  ctssdc  7172  infnninf  7183  infnninfOLD  7184  nnnninfeq  7187  exmidonfinlem  7253  exmidmotap  7321  addcmpblnq  7427  distrnqg  7447  ltexnqq  7468  addcmpblnq0  7503  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  nq0a0  7517  nnanq0  7518  distrnq0  7519  prarloclemlo  7554  prarloclemcalc  7562  genpassl  7584  genpassu  7585  ltsosr  7824  0idsr  7827  1idsr  7828  mulextsr1lem  7840  cnegex  8197  subsub3  8251  subadd4  8263  mulneg12  8416  mulsub  8420  apreap  8606  cru  8621  recextlem1  8670  cju  8980  ofnegsub  8981  halfaddsub  9216  nn0supp  9292  nneo  9420  zeo2  9423  uzin  9625  xaddcom  9927  xaddass  9935  xleaddadd  9953  iccf1o  10070  fzsuc2  10145  fldiv4lem1div2uz2  10375  flqeqceilz  10389  zmod1congr  10412  modqcyc  10430  modqcyc2  10431  modqaddabs  10433  modqmul1  10448  modqaddmulmod  10462  addmodlteq  10469  frec2uzrdg  10480  frecuzrdgsuctlem  10494  seq3val  10531  seqvalcd  10532  seq3fveq2  10546  seqfveq2g  10548  seq3split  10559  seqsplitg  10560  seqf1oglem2a  10589  seqf1oglem2  10591  seqfeq4g  10602  seq3distr  10603  ser0f  10605  expp1  10617  mulexp  10649  mulexpzap  10650  expadd  10652  expaddzap  10654  expmul  10655  expmulzap  10656  expsubap  10658  expdivap  10661  subsq  10717  mulbinom2  10727  binom3  10728  bernneq  10731  modqexp  10737  nn0opthd  10793  faclbnd  10812  faclbnd6  10815  bccmpl  10825  bcp1n  10832  zfz1isolemiso  10910  seq3coll  10913  shftval2  10970  shftval4  10972  seq3shft  10982  crre  11001  remim  11004  remullem  11015  cjexp  11037  cnrecnv  11054  resqrexlemlo  11157  resqrexlemcalc1  11158  resqrexlemcalc2  11159  resqrexlemcalc3  11160  resqrexlemnm  11162  rsqrmo  11171  abscj  11196  absid  11215  absre  11221  recvalap  11241  maxabsle  11348  maxltsup  11362  2zsupmax  11369  minabs  11379  bdtrilem  11382  bdtri  11383  2zinfmin  11386  xrmaxiflemab  11390  xrmaxiflemcom  11392  xrmaxadd  11404  xrbdtri  11419  iooinsup  11420  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  climcvg1nlem  11492  summodclem3  11523  zsumdc  11527  isum  11528  isumz  11532  isumss  11534  fisumss  11535  fsum3cvg2  11537  fsumadd  11549  isummulc2  11569  sumsplitdc  11575  fsum2dlemstep  11577  fisumcom2  11581  fisum0diag2  11590  fsumconst  11597  telfsumo  11609  fsumparts  11613  fsumrelem  11614  binomlem  11626  isumshft  11633  isumsplit  11634  arisum  11641  arisum2  11642  trireciplem  11643  geolim2  11655  geo2sum  11657  0.999...  11664  cvgratz  11675  mertensabs  11680  clim2prod  11682  prodf1f  11686  prodmodclem2a  11719  zproddc  11722  iprodap  11723  iprodap0  11725  fprodseq  11726  prod1dc  11729  prodssdc  11732  fprod2dlemstep  11765  fprodcom2fi  11769  fproddivap  11773  ef0lem  11803  efval2  11808  ege2le3  11814  efaddlem  11817  efsub  11824  eftlub  11833  efsep  11834  tanval3ap  11857  efi4p  11860  sinneg  11869  sinmul  11887  sincossq  11891  cos2t  11893  demoivreALT  11917  eirraplem  11920  dvdsmodexp  11938  odd2np1  12014  omoe  12037  divalglemex  12063  divalglemeuneg  12064  divalgmod  12068  flodddiv4  12075  gcdneg  12119  gcdaddm  12121  modgcd  12128  bezoutlemnewy  12133  gcdass  12152  gcdmultiple  12157  nninfctlemfo  12177  algrp1  12184  lcmneg  12212  lcmgcdeq  12221  lcmass  12223  cncongr2  12242  prmexpb  12289  sqrt2irr  12300  2sqpwodd  12314  qnumdenbi  12330  phiprmpw  12360  eulerthlema  12368  fermltl  12372  prmdiveq  12374  modprm0  12392  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  pythagtriplem19  12420  pcpremul  12431  pcneg  12463  pcgcd  12467  pc2dvds  12468  pcaddlem  12477  pcprod  12484  fldivp1  12486  pcbc  12489  prmpwdvds  12493  pockthlem  12494  mul4sqlem  12531  4sqlem11  12539  4sqlem12  12540  4sqlem17  12545  ctiunctlemfo  12596  strslfv3  12664  ressval3d  12690  resseqnbasd  12691  imasival  12889  qusval  12906  plusfeqg  12947  sgrp1  12994  idmhm  13041  resmhm2  13060  mhmeql  13064  grppropstrg  13091  grpinvinv  13139  grp1  13178  imasgrp2  13180  mulgnngsum  13197  mulginvcom  13217  mulgnndir  13221  mulgdir  13224  mulgneg2  13226  mulgnnass  13227  mulgass  13229  mulgsubdir  13232  trivsubgd  13270  nmzsubg  13280  qussub  13307  idghm  13329  ablinvadd  13380  ablsub2inv  13381  eqgabl  13400  mgpplusgg  13420  mgpbasg  13422  mgpscag  13423  mgptsetg  13424  mgpdsg  13426  mgpress  13427  srgpcomp  13486  srgpcompp  13487  ringo2times  13524  ring1eq0  13544  ring1  13555  opprmulfvalg  13566  crngoppr  13568  opprsllem  13570  oppr1g  13578  opprunitd  13606  rdivmuldivd  13640  rhmunitinv  13674  scafeqg  13804  lmodvsubval2  13838  lmodsubdi  13840  rmodislmod  13847  sralemg  13934  sraipg  13940  crng2idl  14027  cnfldmulg  14064  cnfldexp  14065  cnfldui  14077  mulgrhm2  14098  zrhrhmb  14110  zlmvscag  14121  znval2  14126  znbaslemnn  14127  znunit  14147  psrval  14152  restuni2  14345  lmfval  14360  cnfval  14362  cnpfval  14363  txtopon  14430  txcnp  14439  upxp  14440  txrest  14444  cnmptcom  14466  bl2in  14571  xblss2  14573  isxms2  14620  setsmsdsg  14648  setsmstsetg  14649  metss  14662  resubmet  14716  cncfcncntop  14748  dvidlemap  14845  dvcnp2cntop  14848  dvcoapbr  14856  dvcjbr  14857  dvexp  14860  dvexp2  14861  dvrecap  14862  plyaddlem1  14893  plymullem1  14894  efimpi  14954  tangtx  14973  logdivlti  15016  cxpexprp  15030  rpcxpsub  15043  rpabscxpbnd  15073  rprelogbdiv  15089  binom4  15111  lgslem1  15116  lgsmod  15142  lgsdilem  15143  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  lgseisenlem2  15187  lgseisenlem3  15188  2lgsoddprmlem2  15194  2sqlem4  15205  bj-charfundcALT  15301  1dom1el  15483  sssneq  15492  0nninf  15494  trilpolemisumle  15528