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  3573  ifeq1dadc  3591  ifeq2dadc  3592  eqifdc  3596  ifnotdc  3598  ifandc  3599  ifordc  3600  onsucuni2  4600  relop  4816  riinint  4927  iotauni  5231  fniinfv  5619  fsn2  5736  fmptapd  5753  fconst2g  5777  fniunfv  5809  ofres  6150  ofco  6154  frecsuclem  6464  frecrdg  6466  oasuc  6522  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  funresdfunsndc  6564  uniqs2  6654  en1bg  6859  fundmen  6865  1domsn  6878  pw2f1odclem  6895  mapxpen  6909  xpmapenlem  6910  phplem4dom  6923  en2eqpr  6968  sbthlemi5  7027  omp1eomlem  7160  difinfsnlem  7165  ctmlemr  7174  ctssdccl  7177  ctssdc  7179  infnninf  7190  infnninfOLD  7191  nnnninfeq  7194  exmidonfinlem  7260  exmidmotap  7328  addcmpblnq  7434  distrnqg  7454  ltexnqq  7475  addcmpblnq0  7510  nqnq0a  7521  nqnq0m  7522  nq0m0r  7523  nq0a0  7524  nnanq0  7525  distrnq0  7526  prarloclemlo  7561  prarloclemcalc  7569  genpassl  7591  genpassu  7592  ltsosr  7831  0idsr  7834  1idsr  7835  mulextsr1lem  7847  cnegex  8204  subsub3  8258  subadd4  8270  mulneg12  8423  mulsub  8427  apreap  8614  cru  8629  recextlem1  8678  cju  8988  ofnegsub  8989  halfaddsub  9225  nn0supp  9301  nneo  9429  zeo2  9432  uzin  9634  xaddcom  9936  xaddass  9944  xleaddadd  9962  iccf1o  10079  fzsuc2  10154  fldiv4lem1div2uz2  10396  flqeqceilz  10410  zmod1congr  10433  modqcyc  10451  modqcyc2  10452  modqaddabs  10454  modqmul1  10469  modqaddmulmod  10483  addmodlteq  10490  frec2uzrdg  10501  frecuzrdgsuctlem  10515  seq3val  10552  seqvalcd  10553  seq3fveq2  10567  seqfveq2g  10569  seq3split  10580  seqsplitg  10581  seqf1oglem2a  10610  seqf1oglem2  10612  seqfeq4g  10623  seq3distr  10624  ser0f  10626  expp1  10638  mulexp  10670  mulexpzap  10671  expadd  10673  expaddzap  10675  expmul  10676  expmulzap  10677  expsubap  10679  expdivap  10682  subsq  10738  mulbinom2  10748  binom3  10749  bernneq  10752  modqexp  10758  nn0opthd  10814  faclbnd  10833  faclbnd6  10836  bccmpl  10846  bcp1n  10853  zfz1isolemiso  10931  seq3coll  10934  shftval2  10991  shftval4  10993  seq3shft  11003  crre  11022  remim  11025  remullem  11036  cjexp  11058  cnrecnv  11075  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnm  11183  rsqrmo  11192  abscj  11217  absid  11236  absre  11242  recvalap  11262  maxabsle  11369  maxltsup  11383  2zsupmax  11391  minabs  11401  bdtrilem  11404  bdtri  11405  2zinfmin  11408  xrmaxiflemab  11412  xrmaxiflemcom  11414  xrmaxadd  11426  xrbdtri  11441  iooinsup  11442  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  climcvg1nlem  11514  summodclem3  11545  zsumdc  11549  isum  11550  isumz  11554  isumss  11556  fisumss  11557  fsum3cvg2  11559  fsumadd  11571  isummulc2  11591  sumsplitdc  11597  fsum2dlemstep  11599  fisumcom2  11603  fisum0diag2  11612  fsumconst  11619  telfsumo  11631  fsumparts  11635  fsumrelem  11636  binomlem  11648  isumshft  11655  isumsplit  11656  arisum  11663  arisum2  11664  trireciplem  11665  geolim2  11677  geo2sum  11679  0.999...  11686  cvgratz  11697  mertensabs  11702  clim2prod  11704  prodf1f  11708  prodmodclem2a  11741  zproddc  11744  iprodap  11745  iprodap0  11747  fprodseq  11748  prod1dc  11751  prodssdc  11754  fprod2dlemstep  11787  fprodcom2fi  11791  fproddivap  11795  ef0lem  11825  efval2  11830  ege2le3  11836  efaddlem  11839  efsub  11846  eftlub  11855  efsep  11856  tanval3ap  11879  efi4p  11882  sinneg  11891  sinmul  11909  sincossq  11913  cos2t  11915  demoivreALT  11939  eirraplem  11942  dvdsmodexp  11960  odd2np1  12038  omoe  12061  divalglemex  12087  divalglemeuneg  12088  divalgmod  12092  flodddiv4  12101  bitsp1  12115  gcdneg  12149  gcdaddm  12151  modgcd  12158  bezoutlemnewy  12163  gcdass  12182  gcdmultiple  12187  nninfctlemfo  12207  algrp1  12214  lcmneg  12242  lcmgcdeq  12251  lcmass  12253  cncongr2  12272  prmexpb  12319  sqrt2irr  12330  2sqpwodd  12344  qnumdenbi  12360  phiprmpw  12390  eulerthlema  12398  fermltl  12402  prmdiveq  12404  modprm0  12423  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  pythagtriplem19  12451  pcpremul  12462  pcneg  12494  pcgcd  12498  pc2dvds  12499  pcaddlem  12508  pcprod  12515  fldivp1  12517  pcbc  12520  prmpwdvds  12524  pockthlem  12525  mul4sqlem  12562  4sqlem11  12570  4sqlem12  12571  4sqlem17  12576  ctiunctlemfo  12656  strslfv3  12724  ressval3d  12750  resseqnbasd  12751  imasival  12949  qusval  12966  plusfeqg  13007  sgrp1  13054  idmhm  13101  resmhm2  13120  mhmeql  13124  grppropstrg  13151  grpinvinv  13199  grp1  13238  imasgrp2  13240  mulgnngsum  13257  mulginvcom  13277  mulgnndir  13281  mulgdir  13284  mulgneg2  13286  mulgnnass  13287  mulgass  13289  mulgsubdir  13292  trivsubgd  13330  nmzsubg  13340  qussub  13367  idghm  13389  ablinvadd  13440  ablsub2inv  13441  eqgabl  13460  mgpplusgg  13480  mgpbasg  13482  mgpscag  13483  mgptsetg  13484  mgpdsg  13486  mgpress  13487  srgpcomp  13546  srgpcompp  13547  ringo2times  13584  ring1eq0  13604  ring1  13615  opprmulfvalg  13626  crngoppr  13628  opprsllem  13630  oppr1g  13638  opprunitd  13666  rdivmuldivd  13700  rhmunitinv  13734  scafeqg  13864  lmodvsubval2  13898  lmodsubdi  13900  rmodislmod  13907  sralemg  13994  sraipg  14000  crng2idl  14087  cnfldmulg  14132  cnfldexp  14133  cnfldui  14145  mulgrhm2  14166  zrhrhmb  14178  zlmvscag  14189  znval2  14194  znbaslemnn  14195  znunit  14215  psrval  14220  restuni2  14413  lmfval  14428  cnfval  14430  cnpfval  14431  txtopon  14498  txcnp  14507  upxp  14508  txrest  14512  cnmptcom  14534  bl2in  14639  xblss2  14641  isxms2  14688  setsmsdsg  14716  setsmstsetg  14717  metss  14730  resubmet  14792  expcn  14805  cncfcncntop  14829  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvcoapbr  14943  dvcjbr  14944  dvexp  14947  dvexp2  14948  dvrecap  14949  plyaddlem1  14983  plymullem1  14984  plycolemc  14994  plycjlemc  14996  dvply1  15001  efimpi  15055  tangtx  15074  logdivlti  15117  cxpexprp  15131  rpcxpsub  15144  rpabscxpbnd  15176  rprelogbdiv  15193  binom4  15215  mpodvdsmulf1o  15226  0sgmppw  15229  lgslem1  15241  lgsmod  15267  lgsdilem  15268  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad3  15325  2lgslem3  15342  2lgsoddprmlem2  15347  2sqlem4  15359  bj-charfundcALT  15455  1dom1el  15637  sssneq  15646  0nninf  15648  trilpolemisumle  15682