Theorem eqtr4d 2240

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtr2d  2243  3eqtr2rd  2244  3eqtr4d  2247  3eqtr4rd  2248  3eqtr4a  2263  sbnfc2  3153  ifsbdc  3582  ifeq1dadc  3600  ifeq2dadc  3601  eqifdc  3606  ifnotdc  3608  ifandc  3609  ifordc  3610  onsucuni2  4610  relop  4826  riinint  4937  iotauni  5241  fniinfv  5631  fsn2  5748  fmptapd  5765  fconst2g  5789  fniunfv  5821  ofres  6163  ofco  6167  caofid1  6177  caofid2  6178  frecsuclem  6482  frecrdg  6484  oasuc  6540  nnacom  6560  nnaass  6561  nndi  6562  nnmass  6563  nnmsucr  6564  nnmcom  6565  funresdfunsndc  6582  uniqs2  6672  en1bg  6877  fundmen  6883  1domsn  6896  pw2f1odclem  6913  mapxpen  6927  xpmapenlem  6928  phplem4dom  6941  en2eqpr  6986  sbthlemi5  7045  omp1eomlem  7178  difinfsnlem  7183  ctmlemr  7192  ctssdccl  7195  ctssdc  7197  infnninf  7208  infnninfOLD  7209  nnnninfeq  7212  exmidonfinlem  7283  exmidmotap  7355  addcmpblnq  7462  distrnqg  7482  ltexnqq  7503  addcmpblnq0  7538  nqnq0a  7549  nqnq0m  7550  nq0m0r  7551  nq0a0  7552  nnanq0  7553  distrnq0  7554  prarloclemlo  7589  prarloclemcalc  7597  genpassl  7619  genpassu  7620  ltsosr  7859  0idsr  7862  1idsr  7863  mulextsr1lem  7875  cnegex  8232  subsub3  8286  subadd4  8298  mulneg12  8451  mulsub  8455  apreap  8642  cru  8657  recextlem1  8706  cju  9016  ofnegsub  9017  halfaddsub  9253  nn0supp  9329  nneo  9458  zeo2  9461  uzin  9663  xaddcom  9965  xaddass  9973  xleaddadd  9991  iccf1o  10108  fzsuc2  10183  fldiv4lem1div2uz2  10430  flqeqceilz  10444  zmod1congr  10467  modqcyc  10485  modqcyc2  10486  modqaddabs  10488  modqmul1  10503  modqaddmulmod  10517  addmodlteq  10524  frec2uzrdg  10535  frecuzrdgsuctlem  10549  seq3val  10586  seqvalcd  10587  seq3fveq2  10601  seqfveq2g  10603  seq3split  10614  seqsplitg  10615  seqf1oglem2a  10644  seqf1oglem2  10646  seqfeq4g  10657  seq3distr  10658  ser0f  10660  expp1  10672  mulexp  10704  mulexpzap  10705  expadd  10707  expaddzap  10709  expmul  10710  expmulzap  10711  expsubap  10713  expdivap  10716  subsq  10772  mulbinom2  10782  binom3  10783  bernneq  10786  modqexp  10792  nn0opthd  10848  faclbnd  10867  faclbnd6  10870  bccmpl  10880  bcp1n  10887  zfz1isolemiso  10965  seq3coll  10968  ccatsymb  11033  ccatval1lsw  11035  ccatass  11039  shftval2  11056  shftval4  11058  seq3shft  11068  crre  11087  remim  11090  remullem  11101  cjexp  11123  cnrecnv  11140  resqrexlemlo  11243  resqrexlemcalc1  11244  resqrexlemcalc2  11245  resqrexlemcalc3  11246  resqrexlemnm  11248  rsqrmo  11257  abscj  11282  absid  11301  absre  11307  recvalap  11327  maxabsle  11434  maxltsup  11448  2zsupmax  11456  minabs  11466  bdtrilem  11469  bdtri  11470  2zinfmin  11473  xrmaxiflemab  11477  xrmaxiflemcom  11479  xrmaxadd  11491  xrbdtri  11506  iooinsup  11507  climaddc1  11559  climmulc2  11561  climsubc1  11562  climsubc2  11563  climcvg1nlem  11579  summodclem3  11610  zsumdc  11614  isum  11615  isumz  11619  isumss  11621  fisumss  11622  fsum3cvg2  11624  fsumadd  11636  isummulc2  11656  sumsplitdc  11662  fsum2dlemstep  11664  fisumcom2  11668  fisum0diag2  11677  fsumconst  11684  telfsumo  11696  fsumparts  11700  fsumrelem  11701  binomlem  11713  isumshft  11720  isumsplit  11721  arisum  11728  arisum2  11729  trireciplem  11730  geolim2  11742  geo2sum  11744  0.999...  11751  cvgratz  11762  mertensabs  11767  clim2prod  11769  prodf1f  11773  prodmodclem2a  11806  zproddc  11809  iprodap  11810  iprodap0  11812  fprodseq  11813  prod1dc  11816  prodssdc  11819  fprod2dlemstep  11852  fprodcom2fi  11856  fproddivap  11860  ef0lem  11890  efval2  11895  ege2le3  11901  efaddlem  11904  efsub  11911  eftlub  11920  efsep  11921  tanval3ap  11944  efi4p  11947  sinneg  11956  sinmul  11974  sincossq  11978  cos2t  11980  demoivreALT  12004  eirraplem  12007  dvdsmodexp  12025  odd2np1  12103  omoe  12126  divalglemex  12152  divalglemeuneg  12153  divalgmod  12157  flodddiv4  12166  bitsp1  12181  bitsinv1lem  12191  bitsinv1  12192  gcdneg  12222  gcdaddm  12224  modgcd  12231  bezoutlemnewy  12236  gcdass  12255  gcdmultiple  12260  nninfctlemfo  12280  algrp1  12287  lcmneg  12315  lcmgcdeq  12324  lcmass  12326  cncongr2  12345  prmexpb  12392  sqrt2irr  12403  2sqpwodd  12417  qnumdenbi  12433  phiprmpw  12463  eulerthlema  12471  fermltl  12475  prmdiveq  12477  modprm0  12496  pythagtriplem1  12507  pythagtriplem12  12517  pythagtriplem14  12519  pythagtriplem15  12520  pythagtriplem16  12521  pythagtriplem17  12522  pythagtriplem19  12524  pcpremul  12535  pcneg  12567  pcgcd  12571  pc2dvds  12572  pcaddlem  12581  pcprod  12588  fldivp1  12590  pcbc  12593  prmpwdvds  12597  pockthlem  12598  mul4sqlem  12635  4sqlem11  12643  4sqlem12  12644  4sqlem17  12649  ctiunctlemfo  12729  ressval3d  12823  resseqnbasd  12824  prdsval  13023  imasival  13056  qusval  13073  plusfeqg  13114  sgrp1  13161  idmhm  13219  resmhm2  13238  mhmeql  13242  grppropstrg  13269  grpinvinv  13317  grp1  13356  imasgrp2  13364  mulgnngsum  13381  mulginvcom  13401  mulgnndir  13405  mulgdir  13408  mulgneg2  13410  mulgnnass  13411  mulgass  13413  mulgsubdir  13416  trivsubgd  13454  nmzsubg  13464  qussub  13491  idghm  13513  ablinvadd  13564  ablsub2inv  13565  eqgabl  13584  mgpplusgg  13604  mgpbasg  13606  mgpscag  13607  mgptsetg  13608  mgpdsg  13610  mgpress  13611  srgpcomp  13670  srgpcompp  13671  ringo2times  13708  ring1eq0  13728  ring1  13739  opprmulfvalg  13750  crngoppr  13752  opprsllem  13754  oppr1g  13762  opprunitd  13790  rdivmuldivd  13824  rhmunitinv  13858  scafeqg  13988  lmodvsubval2  14022  lmodsubdi  14024  rmodislmod  14031  sralemg  14118  sraipg  14124  crng2idl  14211  cnfldmulg  14256  cnfldexp  14257  cnfldui  14269  mulgrhm2  14290  zrhrhmb  14302  zlmvscag  14313  znval2  14318  znbaslemnn  14319  znunit  14339  psrval  14346  psrgrp  14365  psrneg  14367  mplval2g  14375  restuni2  14567  lmfval  14582  cnfval  14584  cnpfval  14585  txtopon  14652  txcnp  14661  upxp  14662  txrest  14666  cnmptcom  14688  bl2in  14793  xblss2  14795  isxms2  14842  setsmsdsg  14870  setsmstsetg  14871  metss  14884  resubmet  14946  expcn  14959  cncfcncntop  14983  dvidlemap  15081  dvidrelem  15082  dvidsslem  15083  dvcnp2cntop  15089  dvcoapbr  15097  dvcjbr  15098  dvexp  15101  dvexp2  15102  dvrecap  15103  plyaddlem1  15137  plymullem1  15138  plycolemc  15148  plycjlemc  15150  dvply1  15155  efimpi  15209  tangtx  15228  logdivlti  15271  cxpexprp  15285  rpcxpsub  15298  rpabscxpbnd  15330  rprelogbdiv  15347  binom4  15369  mpodvdsmulf1o  15380  0sgmppw  15383  lgslem1  15395  lgsmod  15421  lgsdilem  15422  lgsdi  15432  lgsne0  15433  lgsdirnn0  15442  lgsdinn0  15443  lgseisenlem2  15466  lgseisenlem3  15467  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad2lem1  15476  lgsquad3  15479  2lgslem3  15496  2lgsoddprmlem2  15501  2sqlem4  15513  bj-charfundcALT  15609  1dom1el  15791  2omap  15796  sssneq  15803  0nninf  15805  nnnninfex  15823  nninfnfiinf  15824  trilpolemisumle  15841