Theorem eqtr4d 2242

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  3eqtr2d  2245  3eqtr2rd  2246  3eqtr4d  2249  3eqtr4rd  2250  3eqtr4a  2265  sbnfc2  3158  ifsbdc  3588  ifeq1dadc  3606  ifeq2dadc  3607  eqifdc  3612  ifnotdc  3614  ifandc  3615  ifordc  3616  onsucuni2  4620  relop  4836  riinint  4948  iotauni  5253  fniinfv  5650  fsn2  5767  fmptapd  5788  fconst2g  5812  fniunfv  5844  ofres  6186  ofco  6190  caofid1  6200  caofid2  6201  frecsuclem  6505  frecrdg  6507  oasuc  6563  nnacom  6583  nnaass  6584  nndi  6585  nnmass  6586  nnmsucr  6587  nnmcom  6588  funresdfunsndc  6605  uniqs2  6695  en1bg  6905  fundmen  6912  1domsn  6929  pw2f1odclem  6946  mapxpen  6960  xpmapenlem  6961  phplem4dom  6974  en2eqpr  7019  sbthlemi5  7078  omp1eomlem  7211  difinfsnlem  7216  ctmlemr  7225  ctssdccl  7228  ctssdc  7230  infnninf  7241  infnninfOLD  7242  nnnninfeq  7245  exmidonfinlem  7317  exmidmotap  7393  addcmpblnq  7500  distrnqg  7520  ltexnqq  7541  addcmpblnq0  7576  nqnq0a  7587  nqnq0m  7588  nq0m0r  7589  nq0a0  7590  nnanq0  7591  distrnq0  7592  prarloclemlo  7627  prarloclemcalc  7635  genpassl  7657  genpassu  7658  ltsosr  7897  0idsr  7900  1idsr  7901  mulextsr1lem  7913  cnegex  8270  subsub3  8324  subadd4  8336  mulneg12  8489  mulsub  8493  apreap  8680  cru  8695  recextlem1  8744  cju  9054  ofnegsub  9055  halfaddsub  9291  nn0supp  9367  nneo  9496  zeo2  9499  uzin  9701  xaddcom  10003  xaddass  10011  xleaddadd  10029  iccf1o  10146  fzsuc2  10221  fldiv4lem1div2uz2  10471  flqeqceilz  10485  zmod1congr  10508  modqcyc  10526  modqcyc2  10527  modqaddabs  10529  modqmul1  10544  modqaddmulmod  10558  addmodlteq  10565  frec2uzrdg  10576  frecuzrdgsuctlem  10590  seq3val  10627  seqvalcd  10628  seq3fveq2  10642  seqfveq2g  10644  seq3split  10655  seqsplitg  10656  seqf1oglem2a  10685  seqf1oglem2  10687  seqfeq4g  10698  seq3distr  10699  ser0f  10701  expp1  10713  mulexp  10745  mulexpzap  10746  expadd  10748  expaddzap  10750  expmul  10751  expmulzap  10752  expsubap  10754  expdivap  10757  subsq  10813  mulbinom2  10823  binom3  10824  bernneq  10827  modqexp  10833  nn0opthd  10889  faclbnd  10908  faclbnd6  10911  bccmpl  10921  bcp1n  10928  zfz1isolemiso  11006  seq3coll  11009  ccatsymb  11081  ccatval1lsw  11083  ccatass  11087  eqs1  11105  lswccats1fst  11119  swrdsb0eq  11141  swrdsbslen  11142  swrds1  11144  ccatswrd  11146  pfxres  11157  ccatpfx  11177  pfxpfx  11184  cats1un  11197  shftval2  11212  shftval4  11214  seq3shft  11224  crre  11243  remim  11246  remullem  11257  cjexp  11279  cnrecnv  11296  resqrexlemlo  11399  resqrexlemcalc1  11400  resqrexlemcalc2  11401  resqrexlemcalc3  11402  resqrexlemnm  11404  rsqrmo  11413  abscj  11438  absid  11457  absre  11463  recvalap  11483  maxabsle  11590  maxltsup  11604  2zsupmax  11612  minabs  11622  bdtrilem  11625  bdtri  11626  2zinfmin  11629  xrmaxiflemab  11633  xrmaxiflemcom  11635  xrmaxadd  11647  xrbdtri  11662  iooinsup  11663  climaddc1  11715  climmulc2  11717  climsubc1  11718  climsubc2  11719  climcvg1nlem  11735  summodclem3  11766  zsumdc  11770  isum  11771  isumz  11775  isumss  11777  fisumss  11778  fsum3cvg2  11780  fsumadd  11792  isummulc2  11812  sumsplitdc  11818  fsum2dlemstep  11820  fisumcom2  11824  fisum0diag2  11833  fsumconst  11840  telfsumo  11852  fsumparts  11856  fsumrelem  11857  binomlem  11869  isumshft  11876  isumsplit  11877  arisum  11884  arisum2  11885  trireciplem  11886  geolim2  11898  geo2sum  11900  0.999...  11907  cvgratz  11918  mertensabs  11923  clim2prod  11925  prodf1f  11929  prodmodclem2a  11962  zproddc  11965  iprodap  11966  iprodap0  11968  fprodseq  11969  prod1dc  11972  prodssdc  11975  fprod2dlemstep  12008  fprodcom2fi  12012  fproddivap  12016  ef0lem  12046  efval2  12051  ege2le3  12057  efaddlem  12060  efsub  12067  eftlub  12076  efsep  12077  tanval3ap  12100  efi4p  12103  sinneg  12112  sinmul  12130  sincossq  12134  cos2t  12136  demoivreALT  12160  eirraplem  12163  dvdsmodexp  12181  odd2np1  12259  omoe  12282  divalglemex  12308  divalglemeuneg  12309  divalgmod  12313  flodddiv4  12322  bitsp1  12337  bitsinv1lem  12347  bitsinv1  12348  gcdneg  12378  gcdaddm  12380  modgcd  12387  bezoutlemnewy  12392  gcdass  12411  gcdmultiple  12416  nninfctlemfo  12436  algrp1  12443  lcmneg  12471  lcmgcdeq  12480  lcmass  12482  cncongr2  12501  prmexpb  12548  sqrt2irr  12559  2sqpwodd  12573  qnumdenbi  12589  phiprmpw  12619  eulerthlema  12627  fermltl  12631  prmdiveq  12633  modprm0  12652  pythagtriplem1  12663  pythagtriplem12  12673  pythagtriplem14  12675  pythagtriplem15  12676  pythagtriplem16  12677  pythagtriplem17  12678  pythagtriplem19  12680  pcpremul  12691  pcneg  12723  pcgcd  12727  pc2dvds  12728  pcaddlem  12737  pcprod  12744  fldivp1  12746  pcbc  12749  prmpwdvds  12753  pockthlem  12754  mul4sqlem  12791  4sqlem11  12799  4sqlem12  12800  4sqlem17  12805  ctiunctlemfo  12885  ressval3d  12979  resseqnbasd  12980  prdsval  13180  imasival  13213  qusval  13230  plusfeqg  13271  sgrp1  13318  idmhm  13376  resmhm2  13395  mhmeql  13399  grppropstrg  13426  grpinvinv  13474  grp1  13513  imasgrp2  13521  mulgnngsum  13538  mulginvcom  13558  mulgnndir  13562  mulgdir  13565  mulgneg2  13567  mulgnnass  13568  mulgass  13570  mulgsubdir  13573  trivsubgd  13611  nmzsubg  13621  qussub  13648  idghm  13670  ablinvadd  13721  ablsub2inv  13722  eqgabl  13741  mgpplusgg  13761  mgpbasg  13763  mgpscag  13764  mgptsetg  13765  mgpdsg  13767  mgpress  13768  srgpcomp  13827  srgpcompp  13828  ringo2times  13865  ring1eq0  13885  ring1  13896  opprmulfvalg  13907  crngoppr  13909  opprsllem  13911  oppr1g  13919  opprunitd  13947  rdivmuldivd  13981  rhmunitinv  14015  scafeqg  14145  lmodvsubval2  14179  lmodsubdi  14181  rmodislmod  14188  sralemg  14275  sraipg  14281  crng2idl  14368  cnfldmulg  14413  cnfldexp  14414  cnfldui  14426  mulgrhm2  14447  zrhrhmb  14459  zlmvscag  14470  znval2  14475  znbaslemnn  14476  znunit  14496  psrval  14503  psrgrp  14522  psrneg  14524  mplval2g  14532  restuni2  14724  lmfval  14739  cnfval  14741  cnpfval  14742  txtopon  14809  txcnp  14818  upxp  14819  txrest  14823  cnmptcom  14845  bl2in  14950  xblss2  14952  isxms2  14999  setsmsdsg  15027  setsmstsetg  15028  metss  15041  resubmet  15103  expcn  15116  cncfcncntop  15140  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvcnp2cntop  15246  dvcoapbr  15254  dvcjbr  15255  dvexp  15258  dvexp2  15259  dvrecap  15260  plyaddlem1  15294  plymullem1  15295  plycolemc  15305  plycjlemc  15307  dvply1  15312  efimpi  15366  tangtx  15385  logdivlti  15428  cxpexprp  15442  rpcxpsub  15455  rpabscxpbnd  15487  rprelogbdiv  15504  binom4  15526  mpodvdsmulf1o  15537  0sgmppw  15540  lgslem1  15552  lgsmod  15578  lgsdilem  15579  lgsdi  15589  lgsne0  15590  lgsdirnn0  15599  lgsdinn0  15600  lgseisenlem2  15623  lgseisenlem3  15624  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2lem1  15633  lgsquad3  15636  2lgslem3  15653  2lgsoddprmlem2  15658  2sqlem4  15670  basvtxval2dom  15708  edgfiedgval2dom  15709  bj-charfundcALT  15883  1dom1el  16065  2omap  16071  sssneq  16080  0nninf  16082  nnnninfex  16100  nninfnfiinf  16101  trilpolemisumle  16118