Theorem eqtr3d 2241

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 2212	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqtr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 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:  3eqtr3d  2247  3eqtr3rd  2248  3eqtr3a  2263  opth  4286  eusvnf  4505  f00  5476  f1imacnv  5548  foimacnv  5549  f1ococnv1  5560  funfvdm  5652  fvmptdf  5677  fndmdif  5695  funopsn  5772  acexmidlemph  5947  acexmidlemab  5948  ovmpodf  6087  fvmpopr2d  6092  oprssov  6098  tfrlemisucaccv  6421  tfr1onlemsucaccv  6437  tfrcllemsucaccv  6450  oav2  6559  omv2  6561  fnsnsplitdc  6601  ecopovtrn  6729  ecopovtrng  6732  map0b  6784  en1  6901  ssenen  6960  fidifsnen  6979  dif1en  6988  undifdc  7033  fidcenumlemr  7069  ordiso2  7149  nninfninc  7237  nnnninfeq2  7243  nninfisollemne  7245  finomni  7254  exmidomni  7256  fodjum  7260  exmidaclem  7333  distrnqg  7513  1qec  7514  prarloclemarch2  7545  nnnq0lem1  7572  nqpnq0nq  7579  distrnq0  7585  prarloclemlt  7619  prmuloclemcalc  7691  ltaprg  7745  prplnqu  7746  recexprlem1ssl  7759  recexprlem1ssu  7760  ltmprr  7768  cauappcvgprlemopl  7772  caucvgprlemopl  7795  caucvgprprlemopl  7823  caucvgprprlemexb  7833  prsrlem1  7868  ltsosr  7890  mulgt0sr  7904  recidpipr  7982  recriota  8016  nntopi  8020  axcaucvglemres  8025  addlid  8224  readdcan  8225  muladd11r  8241  add32r  8245  cnegexlem2  8261  cnegex  8263  pncan2  8292  addsubass  8295  subadd23  8297  addsub12  8298  subid  8304  subid1  8305  npncan  8306  nppcan3  8309  subsub  8315  nppcan2  8316  nnncan2  8322  npncan3  8323  pnpcan  8324  negdi  8342  mvlraddd  8449  mvlladdd  8450  pnpncand  8460  subdi  8470  mulsub  8486  mulsub2  8487  eqord1  8569  recexap  8739  div32ap  8778  divsubdirap  8794  divmuldivap  8798  divdivdivap  8799  divmuleqap  8803  divcanap6  8805  dmdcanap  8808  divsubdivap  8814  div2negap  8821  div2subap  8923  mvllmulapd  8928  prodgt0gt0  8937  cju  9047  zneo  9487  infrenegsupex  9728  qreccl  9776  mul2lt0rlt0  9894  xnpcan  10007  fzosn  10347  modqid  10507  modqm1p1mod0  10533  modqltm1p1mod  10534  modqmul1  10535  modaddmodup  10545  modaddmodlo  10546  modqsubdir  10551  iseqf1olemkle  10655  iseqf1olemklt  10656  seq3f1olemstep  10672  seq3f1oleml  10674  seqf1oglem2  10678  seqfeq3  10687  seq3distr  10690  expineg2  10706  expm1t  10725  expadd  10739  expaddzaplem  10740  expmulzap  10743  sqsubswap  10757  subsq2  10805  binom2sub  10811  binom3  10815  facndiv  10897  bcval5  10921  bcn2p1  10928  bcnm1  10930  2shfti  11192  shftcan2  11196  reim0  11222  imval2  11255  cjreim2  11265  cjdivap  11270  cnrecnv  11271  rennim  11363  resqrexlemnm  11379  remsqsqrt  11393  sqrtdiv  11403  sqrtmsq  11406  sqabsadd  11416  sqabssub  11417  absreim  11429  absdivap  11431  absnid  11434  sqabs  11443  abslt  11449  absle  11450  recvalap  11458  abssub  11462  maxabslemlub  11568  infxrnegsupex  11624  mulcn2  11673  reccn2ap  11674  cjcn2  11677  summodclem3  11741  summodclem2a  11742  summodc  11744  zsumdc  11745  fsum3  11748  fisumss  11753  fsumcl2lem  11759  fsumm1  11777  fsum1p  11779  isummulc2  11787  telfsumo  11827  binomlem  11844  bcxmas  11850  arisum  11859  trireciplem  11861  trirecip  11862  geolim2  11873  georeclim  11874  cvgratnnlemfm  11890  cvgratz  11893  mertenslemi1  11896  clim2divap  11901  prodmodclem3  11936  prodmodclem2a  11937  zproddc  11940  fprodseq  11944  fprodssdc  11951  fprod1p  11960  efcan  12037  efexp  12043  efzval  12044  efgt0  12045  eftlub  12051  efltim  12059  resinval  12076  recosval  12077  cosmul  12106  cos2t  12111  cos2tsin  12112  cos01bnd  12119  cos12dec  12129  eirraplem  12138  muldvds1  12177  dvdsexp  12222  oexpneg  12238  divalglemqt  12280  divalglemeunn  12282  divalglemeuneg  12284  divalgmod  12288  flodddiv4t2lthalf  12300  bitsmod  12317  bitsinv1lem  12322  gcdid0  12351  gcdaddm  12355  dvdsgcdidd  12365  rpmulgcd  12397  sqgcd  12400  algcvg  12420  eucalgcvga  12430  eucalg  12431  dvdslcm  12441  lcmeq0  12443  lcmgcd  12450  qredeu  12469  sqnprm  12508  divgcdodd  12515  sqrt2irrlem  12533  sqpweven  12547  2sqpwodd  12548  divnumden  12568  hashdvds  12593  phimullem  12597  eulerthlemrprm  12601  eulerthlemth  12604  odzdvds  12618  pythagtriplem3  12640  pythagtriplem4  12641  pythagtriplem14  12650  pythagtriplem19  12655  pcpremul  12666  pceulem  12667  pcqdiv  12680  pcaddlem  12712  fldivp1  12721  1arithlem4  12739  4sqlem10  12760  mul4sqlem  12766  4sqlem11  12774  4sqlem15  12778  4sqlem16  12779  4sqlem17  12780  ennnfonelemhf1o  12834  strslssd  12929  ressbas2d  12950  ressinbasd  12956  topnidg  13134  lidrideqd  13263  grpidd  13265  grprida  13269  gsumress  13277  ismndd  13319  grpidd2  13423  grpinvid1  13434  grpinvid2  13435  grppnpcan2  13476  grpnpncan  13477  dfgrp3mlem  13480  grpsubpropd2  13487  mhmid  13501  mhmmnd  13502  mulgsubcl  13522  mulgneg  13526  mulgaddcomlem  13531  mulginvinv  13534  mulgdirlem  13539  mulgdir  13540  mulgass  13545  mulgmodid  13547  grpissubg  13580  eqgcpbl  13614  ghmid  13635  ghmmulg  13642  resghm  13646  invghm  13715  gsumfzmptfidmadd  13725  mgptopng  13741  srgisid  13798  ringidss  13841  ringcom  13843  opprsubgg  13896  unitgrp  13928  1rinv  13940  0unit  13941  rhmdvdsr  13987  lringuplu  14008  subrngpropd  14028  subrgpropd  14065  lmod0vs  14133  lmodvsmmulgdi  14135  lmodvneg1  14142  lmodcom  14145  lmodsubvs  14155  lmodsubdir  14157  lmodpropd  14161  lspsnsub  14233  lspsneq0b  14239  lsppropd  14244  rlmscabas  14272  lidlbas  14290  zringmulg  14410  restopnb  14703  txcnmpt  14795  cnmpt1t  14807  blhalf  14930  xmspropd  14999  mspropd  15000  mpomulcn  15088  ivthreinc  15167  limcimolemlt  15186  dvfre  15232  dveflem  15248  dvef  15249  ply1termlem  15264  plymullem1  15270  sin2kpi  15333  cos2kpi  15334  sin2pim  15335  cos2pim  15336  ptolemy  15346  sincosq2sgn  15349  sincosq3sgn  15350  sincosq4sgn  15351  sinq12gt0  15352  tangtx  15360  sincosq1eq  15361  abssinper  15368  sinkpi  15369  relogeftb  15387  relogoprlem  15390  relogexp  15394  mpodvdsmulf1o  15512  mersenne  15519  perfectlem1  15521  perfectlem2  15522  perfect  15523  lgsval2lem  15537  lgsdir2lem4  15558  lgsdirprm  15561  lgsdilem2  15563  gausslemma2dlem7  15595  lgseisenlem4  15600  lgsquadlem1  15604  lgsquadlem2  15605  lgsquad2lem1  15608  lgsquad2lem2  15609  2sqlem4  15645  2sqlem6  15647  2sqlem8  15650  peano3nninf  16059  nninfsel  16069  nninffeq  16072  isomninnlem  16084  cvgcmp2nlemabs  16086  trilpolemlt1  16095  trirec0xor  16099  ismkvnnlem  16106