Theorem eqtr3d 2273

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)

Assertion

Ref	Expression
eqtr3d	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2244	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtrd 2271	1 ⊢ (𝜑 → 𝐵 = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3d  2279  3eqtr3rd  2280  3eqtr3a  2295  opth  4377  eusvnf  4599  f00  5584  f1imacnv  5656  foimacnv  5657  f1ococnv1  5668  funfvdm  5766  fvmptdf  5793  fndmdif  5814  funopsn  5891  acexmidlemph  6078  acexmidlemab  6079  ovmpodf  6220  fvmpopr2d  6225  oprssov  6231  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  oav2  6736  omv2  6738  fnsnsplitdc  6778  ecopovtrn  6906  ecopovtrng  6909  map0b  6968  en1  7086  ssenen  7152  fidifsnen  7172  dif1en  7183  undifdc  7231  fidcenumlemr  7272  ordiso2  7376  nninfninc  7464  nnnninfeq2  7470  nninfisollemne  7472  finomni  7481  exmidomni  7483  fodjum  7487  exmidaclem  7565  distrnqg  7755  1qec  7756  prarloclemarch2  7787  nnnq0lem1  7814  nqpnq0nq  7821  distrnq0  7827  prarloclemlt  7861  prmuloclemcalc  7933  ltaprg  7987  prplnqu  7988  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  cauappcvgprlemopl  8014  caucvgprlemopl  8037  caucvgprprlemopl  8065  caucvgprprlemexb  8075  prsrlem1  8110  ltsosr  8132  mulgt0sr  8146  recidpipr  8224  recriota  8258  nntopi  8262  axcaucvglemres  8267  addlid  8467  readdcan  8468  muladd11r  8484  add32r  8488  cnegexlem2  8504  cnegex  8506  pncan2  8535  addsubass  8538  subadd23  8540  addsub12  8541  subid  8547  subid1  8548  npncan  8549  nppcan3  8552  subsub  8558  nppcan2  8559  nnncan2  8565  npncan3  8566  pnpcan  8567  negdi  8585  mvlraddd  8692  mvlladdd  8693  pnpncand  8703  subdi  8714  mulsub  8730  mulsub2  8731  eqord1  8813  recexap  8984  div32ap  9025  divsubdirap  9041  divmuldivap  9045  divdivdivap  9046  divmuleqap  9050  divcanap6  9052  dmdcanap  9055  divsubdivap  9061  div2negap  9068  div2subap  9170  mvllmulapd  9175  prodgt0gt0  9184  cju  9294  zneo  9752  infrenegsupex  10004  qreccl  10052  mul2lt0rlt0  10171  xnpcan  10285  fzosn  10634  modqid  10800  modqm1p1mod0  10826  modqltm1p1mod  10827  modqmul1  10828  modaddmodup  10838  modaddmodlo  10839  modqsubdir  10844  iseqf1olemkle  10948  iseqf1olemklt  10949  seq3f1olemstep  10965  seq3f1oleml  10967  seqf1oglem2  10971  seqfeq3  10980  seq3distr  10983  expineg2  10999  expm1t  11018  expadd  11032  expaddzaplem  11033  expmulzap  11036  sqsubswap  11050  subsq2  11098  binom2sub  11104  binom3  11108  resq01  11109  facndiv  11192  bcval5  11216  bcn2p1  11224  bcnm1  11226  hashpwfi  11284  hashfibclem  11297  pfxccatpfx2  11524  2shfti  11611  shftcan2  11615  reim0  11641  imval2  11674  cjreim2  11685  cjdivap  11690  cnrecnv  11691  rennim  11783  resqrexlemnm  11799  remsqsqrt  11813  sqrtdiv  11823  sqrtmsq  11826  sqabsadd  11836  sqabssub  11837  absreim  11849  absdivap  11851  absnid  11854  sqabs  11864  abslt  11870  absle  11871  recvalap  11879  abssub  11883  maxabslemlub  11989  infxrnegsupex  12047  mulcn2  12096  reccn2ap  12097  cjcn2  12100  summodclem3  12165  summodclem2a  12166  summodc  12168  zsumdc  12169  fsum3  12172  fisumss  12177  fsumcl2lem  12183  fsumm1  12201  fsum1p  12203  isummulc2  12211  telfsumo  12251  binomlem  12268  bcxmas  12274  arisum  12283  trireciplem  12285  trirecip  12286  geolim2  12297  georeclim  12298  cvgratnnlemfm  12314  cvgratz  12317  mertenslemi1  12320  clim2divap  12325  prodmodclem3  12360  prodmodclem2a  12361  zproddc  12364  fprodseq  12368  fprodssdc  12375  fprod1p  12384  efcan  12461  efexp  12467  efzval  12468  efgt0  12469  eftlub  12475  efltim  12483  resinval  12500  recosval  12501  cosmul  12530  cos2t  12535  cos2tsin  12536  cos01bnd  12543  cos12dec  12553  eirraplem  12562  muldvds1  12601  dvdsexp  12646  oexpneg  12662  divalglemqt  12704  divalglemeunn  12706  divalglemeuneg  12708  divalgmod  12712  flodddiv4t2lthalf  12724  bitsmod  12741  bitsinv1lem  12746  gcdid0  12775  gcdaddm  12779  dvdsgcdidd  12789  rpmulgcd  12821  sqgcd  12824  algcvg  12844  eucalgcvga  12854  eucalg  12855  dvdslcm  12865  lcmeq0  12867  lcmgcd  12874  qredeu  12893  sqnprm  12933  divgcdodd  12940  sqrt2irrlem  12958  sqpweven  12973  2sqpwodd  12974  divnumden  12994  hashdvds  13021  phimullem  13025  eulerthlemrprm  13029  eulerthlemth  13032  odzdvds  13046  pythagtriplem3  13068  pythagtriplem4  13069  pythagtriplem14  13078  pythagtriplem19  13083  pcpremul  13094  pceulem  13095  pcqdiv  13108  pcaddlem  13140  fldivp1  13149  1arithlem4  13167  4sqlem10  13188  mul4sqlem  13194  4sqlem11  13202  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemfrceq  13323  ballotfilemrinv0  13327  ennnfonelemhf1o  13355  strslssd  13450  ressbas2d  13473  ressinbasd  13479  topnidg  13657  lidrideqd  13752  grpidd  13754  grprida  13758  gzsumress  13763  ismndd  13801  grpidd2  13897  grpinvid1  13908  grpinvid2  13909  grppnpcan2  13950  grpnpncan  13951  dfgrp3mlem  13954  grpsubpropd2  13961  mhmid  13969  mhmmnd  13970  mulgsubcl  13990  mulgneg  13994  mulgaddcomlem  13999  mulginvinv  14002  mulgdirlem  14007  mulgdir  14008  mulgass  14013  mulgmodid  14015  grpissubg  14048  eqgcpbl  14082  ghmid  14103  ghmmulg  14110  resghm  14114  invghm  14184  gsum0cmn  14205  mgptopng  14279  srgisid  14341  ringidss  14385  ringcom  14387  opprsubgg  14441  unitgrp  14474  1rinv  14486  0unit  14487  rhmdvdsr  14533  lringuplu  14554  subrngpropd  14575  subrgpropd  14612  lmod0vs  14709  lmodvsmmulgdi  14711  lmodvneg1  14718  lmodcom  14721  lmodsubvs  14731  lmodsubdir  14733  lmodpropd  14737  lspsnsub  14809  lspsneq0b  14815  lsppropd  14820  rlmscabas  14848  lidlbas  14866  zringmulg  14984  restopnb  15334  txcnmpt  15426  cnmpt1t  15438  blhalf  15561  xmspropd  15630  mspropd  15631  mpomulcn  15719  ivthreinc  15798  limcimolemlt  15817  dvfre  15863  dveflem  15879  dvef  15880  ply1termlem  15895  plymullem1  15901  sin2kpi  15965  cos2kpi  15966  sin2pim  15967  cos2pim  15968  ptolemy  15978  sincosq2sgn  15981  sincosq3sgn  15982  sincosq4sgn  15983  sinq12gt0  15984  tangtx  15992  sincosq1eq  15993  abssinper  16000  sinkpi  16001  relogeftb  16019  relogoprlem  16023  relogexp  16027  log2tlbndlog2  16142  birthdaylem2  16148  birthdaylem3  16149  pellexlem1  16151  efchtqdvds  16187  ppiqp1le  16189  ppiqltx  16203  mpodvdsmulf1o  16206  ppiqub  16215  chtqub  16218  mersenne  16219  perfectlem1  16221  perfectlem2  16222  perfect  16223  lgsval2lem  16251  lgsdir2lem4  16272  lgsdirprm  16275  lgsdilem2  16277  gausslemma2dlem7  16309  lgseisenlem4  16314  lgsquadlem1  16318  lgsquadlem2  16319  lgsquad2lem1  16322  lgsquad2lem2  16323  2sqlem4  16359  2sqlem6  16361  2sqlem8  16364  clwwlknonel  16795  eupth2fi  16842  dichmul0orlem2  16876  dichmul0orlem3  16877  dichmul0orlem4  16878  peano3nninf  17172  nninfsel  17182  nninffeq  17185  isomninnlem  17201  cvgcmp2nlemabs  17203  trilpolemlt1  17212  trirec0xor  17216  qdiff  17220  ismkvnnlem  17224