Theorem eqtr3d 2231

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 2202	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 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:  3eqtr3d  2237  3eqtr3rd  2238  3eqtr3a  2253  opth  4271  eusvnf  4489  f00  5452  f1imacnv  5524  foimacnv  5525  f1ococnv1  5536  funfvdm  5627  fvmptdf  5652  fndmdif  5670  acexmidlemph  5918  acexmidlemab  5919  ovmpodf  6058  fvmpopr2d  6063  oprssov  6069  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  oav2  6530  omv2  6532  fnsnsplitdc  6572  ecopovtrn  6700  ecopovtrng  6703  map0b  6755  en1  6867  ssenen  6921  fidifsnen  6940  dif1en  6949  undifdc  6994  fidcenumlemr  7030  ordiso2  7110  nninfninc  7198  nnnninfeq2  7204  nninfisollemne  7206  finomni  7215  exmidomni  7217  fodjum  7221  exmidaclem  7293  distrnqg  7473  1qec  7474  prarloclemarch2  7505  nnnq0lem1  7532  nqpnq0nq  7539  distrnq0  7545  prarloclemlt  7579  prmuloclemcalc  7651  ltaprg  7705  prplnqu  7706  recexprlem1ssl  7719  recexprlem1ssu  7720  ltmprr  7728  cauappcvgprlemopl  7732  caucvgprlemopl  7755  caucvgprprlemopl  7783  caucvgprprlemexb  7793  prsrlem1  7828  ltsosr  7850  mulgt0sr  7864  recidpipr  7942  recriota  7976  nntopi  7980  axcaucvglemres  7985  addlid  8184  readdcan  8185  muladd11r  8201  add32r  8205  cnegexlem2  8221  cnegex  8223  pncan2  8252  addsubass  8255  subadd23  8257  addsub12  8258  subid  8264  subid1  8265  npncan  8266  nppcan3  8269  subsub  8275  nppcan2  8276  nnncan2  8282  npncan3  8283  pnpcan  8284  negdi  8302  mvlraddd  8409  mvlladdd  8410  pnpncand  8420  subdi  8430  mulsub  8446  mulsub2  8447  eqord1  8529  recexap  8699  div32ap  8738  divsubdirap  8754  divmuldivap  8758  divdivdivap  8759  divmuleqap  8763  divcanap6  8765  dmdcanap  8768  divsubdivap  8774  div2negap  8781  div2subap  8883  mvllmulapd  8888  prodgt0gt0  8897  cju  9007  zneo  9446  infrenegsupex  9687  qreccl  9735  mul2lt0rlt0  9853  xnpcan  9966  fzosn  10300  modqid  10460  modqm1p1mod0  10486  modqltm1p1mod  10487  modqmul1  10488  modaddmodup  10498  modaddmodlo  10499  modqsubdir  10504  iseqf1olemkle  10608  iseqf1olemklt  10609  seq3f1olemstep  10625  seq3f1oleml  10627  seqf1oglem2  10631  seqfeq3  10640  seq3distr  10643  expineg2  10659  expm1t  10678  expadd  10692  expaddzaplem  10693  expmulzap  10696  sqsubswap  10710  subsq2  10758  binom2sub  10764  binom3  10768  facndiv  10850  bcval5  10874  bcn2p1  10881  bcnm1  10883  2shfti  11015  shftcan2  11019  reim0  11045  imval2  11078  cjreim2  11088  cjdivap  11093  cnrecnv  11094  rennim  11186  resqrexlemnm  11202  remsqsqrt  11216  sqrtdiv  11226  sqrtmsq  11229  sqabsadd  11239  sqabssub  11240  absreim  11252  absdivap  11254  absnid  11257  sqabs  11266  abslt  11272  absle  11273  recvalap  11281  abssub  11285  maxabslemlub  11391  infxrnegsupex  11447  mulcn2  11496  reccn2ap  11497  cjcn2  11500  summodclem3  11564  summodclem2a  11565  summodc  11567  zsumdc  11568  fsum3  11571  fisumss  11576  fsumcl2lem  11582  fsumm1  11600  fsum1p  11602  isummulc2  11610  telfsumo  11650  binomlem  11667  bcxmas  11673  arisum  11682  trireciplem  11684  trirecip  11685  geolim2  11696  georeclim  11697  cvgratnnlemfm  11713  cvgratz  11716  mertenslemi1  11719  clim2divap  11724  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodssdc  11774  fprod1p  11783  efcan  11860  efexp  11866  efzval  11867  efgt0  11868  eftlub  11874  efltim  11882  resinval  11899  recosval  11900  cosmul  11929  cos2t  11934  cos2tsin  11935  cos01bnd  11942  cos12dec  11952  eirraplem  11961  muldvds1  12000  dvdsexp  12045  oexpneg  12061  divalglemqt  12103  divalglemeunn  12105  divalglemeuneg  12107  divalgmod  12111  flodddiv4t2lthalf  12123  bitsmod  12140  bitsinv1lem  12145  gcdid0  12174  gcdaddm  12178  dvdsgcdidd  12188  rpmulgcd  12220  sqgcd  12223  algcvg  12243  eucalgcvga  12253  eucalg  12254  dvdslcm  12264  lcmeq0  12266  lcmgcd  12273  qredeu  12292  sqnprm  12331  divgcdodd  12338  sqrt2irrlem  12356  sqpweven  12370  2sqpwodd  12371  divnumden  12391  hashdvds  12416  phimullem  12420  eulerthlemrprm  12424  eulerthlemth  12427  odzdvds  12441  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem14  12473  pythagtriplem19  12478  pcpremul  12489  pceulem  12490  pcqdiv  12503  pcaddlem  12535  fldivp1  12544  1arithlem4  12562  4sqlem10  12583  mul4sqlem  12589  4sqlem11  12597  4sqlem15  12601  4sqlem16  12602  4sqlem17  12603  ennnfonelemhf1o  12657  strslssd  12752  ressbas2d  12773  ressinbasd  12779  topnidg  12956  lidrideqd  13085  grpidd  13087  grprida  13091  gsumress  13099  ismndd  13141  grpidd2  13245  grpinvid1  13256  grpinvid2  13257  grppnpcan2  13298  grpnpncan  13299  dfgrp3mlem  13302  grpsubpropd2  13309  mhmid  13323  mhmmnd  13324  mulgsubcl  13344  mulgneg  13348  mulgaddcomlem  13353  mulginvinv  13356  mulgdirlem  13361  mulgdir  13362  mulgass  13367  mulgmodid  13369  grpissubg  13402  eqgcpbl  13436  ghmid  13457  ghmmulg  13464  resghm  13468  invghm  13537  gsumfzmptfidmadd  13547  mgptopng  13563  srgisid  13620  ringidss  13663  ringcom  13665  opprsubgg  13718  unitgrp  13750  1rinv  13762  0unit  13763  rhmdvdsr  13809  lringuplu  13830  subrngpropd  13850  subrgpropd  13887  lmod0vs  13955  lmodvsmmulgdi  13957  lmodvneg1  13964  lmodcom  13967  lmodsubvs  13977  lmodsubdir  13979  lmodpropd  13983  lspsnsub  14055  lspsneq0b  14061  lsppropd  14066  rlmscabas  14094  lidlbas  14112  zringmulg  14232  restopnb  14525  txcnmpt  14617  cnmpt1t  14629  blhalf  14752  xmspropd  14821  mspropd  14822  mpomulcn  14910  ivthreinc  14989  limcimolemlt  15008  dvfre  15054  dveflem  15070  dvef  15071  ply1termlem  15086  plymullem1  15092  sin2kpi  15155  cos2kpi  15156  sin2pim  15157  cos2pim  15158  ptolemy  15168  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  tangtx  15182  sincosq1eq  15183  abssinper  15190  sinkpi  15191  relogeftb  15209  relogoprlem  15212  relogexp  15216  mpodvdsmulf1o  15334  mersenne  15341  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsval2lem  15359  lgsdir2lem4  15380  lgsdirprm  15383  lgsdilem2  15385  gausslemma2dlem7  15417  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  lgsquad2lem2  15431  2sqlem4  15467  2sqlem6  15469  2sqlem8  15472  peano3nninf  15762  nninfsel  15772  nninffeq  15775  isomninnlem  15787  cvgcmp2nlemabs  15789  trilpolemlt1  15798  trirec0xor  15802  ismkvnnlem  15809