Theorem eqtr3d 2212

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3d  2218  3eqtr3rd  2219  3eqtr3a  2234  opth  4238  eusvnf  4454  f00  5408  f1imacnv  5479  foimacnv  5480  f1ococnv1  5491  funfvdm  5580  fvmptdf  5604  fndmdif  5622  acexmidlemph  5868  acexmidlemab  5869  ovmpodf  6006  oprssov  6016  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  oav2  6464  omv2  6466  fnsnsplitdc  6506  ecopovtrn  6632  ecopovtrng  6635  map0b  6687  en1  6799  ssenen  6851  fidifsnen  6870  dif1en  6879  undifdc  6923  fidcenumlemr  6954  ordiso2  7034  nnnninfeq2  7127  nninfisollemne  7129  finomni  7138  exmidomni  7140  fodjum  7144  exmidaclem  7207  distrnqg  7386  1qec  7387  prarloclemarch2  7418  nnnq0lem1  7445  nqpnq0nq  7452  distrnq0  7458  prarloclemlt  7492  prmuloclemcalc  7564  ltaprg  7618  prplnqu  7619  recexprlem1ssl  7632  recexprlem1ssu  7633  ltmprr  7641  cauappcvgprlemopl  7645  caucvgprlemopl  7668  caucvgprprlemopl  7696  caucvgprprlemexb  7706  prsrlem1  7741  ltsosr  7763  mulgt0sr  7777  recidpipr  7855  recriota  7889  nntopi  7893  axcaucvglemres  7898  addlid  8096  readdcan  8097  muladd11r  8113  add32r  8117  cnegexlem2  8133  cnegex  8135  pncan2  8164  addsubass  8167  subadd23  8169  addsub12  8170  subid  8176  subid1  8177  npncan  8178  nppcan3  8181  subsub  8187  nppcan2  8188  nnncan2  8194  npncan3  8195  pnpcan  8196  negdi  8214  mvlraddd  8321  mvlladdd  8322  pnpncand  8332  subdi  8342  mulsub  8358  mulsub2  8359  eqord1  8440  recexap  8610  div32ap  8649  divsubdirap  8665  divmuldivap  8669  divdivdivap  8670  divmuleqap  8674  divcanap6  8676  dmdcanap  8679  divsubdivap  8685  div2negap  8692  div2subap  8794  mvllmulapd  8799  prodgt0gt0  8808  cju  8918  zneo  9354  infrenegsupex  9594  qreccl  9642  mul2lt0rlt0  9759  xnpcan  9872  fzosn  10205  modqid  10349  modqm1p1mod0  10375  modqltm1p1mod  10376  modqmul1  10377  modaddmodup  10387  modaddmodlo  10388  modqsubdir  10393  iseqf1olemkle  10484  iseqf1olemklt  10485  seq3f1olemstep  10501  seq3f1oleml  10503  seqfeq3  10512  seq3distr  10513  expineg2  10529  expm1t  10548  expadd  10562  expaddzaplem  10563  expmulzap  10566  sqsubswap  10580  subsq2  10628  binom2sub  10634  binom3  10638  facndiv  10719  bcval5  10743  bcn2p1  10750  bcnm1  10752  2shfti  10840  shftcan2  10844  reim0  10870  imval2  10903  cjreim2  10913  cjdivap  10918  cnrecnv  10919  rennim  11011  resqrexlemnm  11027  remsqsqrt  11041  sqrtdiv  11051  sqrtmsq  11054  sqabsadd  11064  sqabssub  11065  absreim  11077  absdivap  11079  absnid  11082  sqabs  11091  abslt  11097  absle  11098  recvalap  11106  abssub  11110  maxabslemlub  11216  infxrnegsupex  11271  mulcn2  11320  reccn2ap  11321  cjcn2  11324  summodclem3  11388  summodclem2a  11389  summodc  11391  zsumdc  11392  fsum3  11395  fisumss  11400  fsumcl2lem  11406  fsumm1  11424  fsum1p  11426  isummulc2  11434  telfsumo  11474  binomlem  11491  bcxmas  11497  arisum  11506  trireciplem  11508  trirecip  11509  geolim2  11520  georeclim  11521  cvgratnnlemfm  11537  cvgratz  11540  mertenslemi1  11543  clim2divap  11548  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodssdc  11598  fprod1p  11607  efcan  11684  efexp  11690  efzval  11691  efgt0  11692  eftlub  11698  efltim  11706  resinval  11723  recosval  11724  cosmul  11753  cos2t  11758  cos2tsin  11759  cos01bnd  11766  cos12dec  11775  eirraplem  11784  muldvds1  11823  dvdsexp  11867  oexpneg  11882  divalglemqt  11924  divalglemeunn  11926  divalglemeuneg  11928  divalgmod  11932  flodddiv4t2lthalf  11942  gcdid0  11981  gcdaddm  11985  dvdsgcdidd  11995  rpmulgcd  12027  sqgcd  12030  algcvg  12048  eucalgcvga  12058  eucalg  12059  dvdslcm  12069  lcmeq0  12071  lcmgcd  12078  qredeu  12097  sqnprm  12136  divgcdodd  12143  sqrt2irrlem  12161  sqpweven  12175  2sqpwodd  12176  divnumden  12196  hashdvds  12221  phimullem  12225  eulerthlemrprm  12229  eulerthlemth  12232  odzdvds  12245  pythagtriplem3  12267  pythagtriplem4  12268  pythagtriplem14  12277  pythagtriplem19  12282  pcpremul  12293  pceulem  12294  pcqdiv  12307  pcaddlem  12338  fldivp1  12346  1arithlem4  12364  4sqlem10  12385  mul4sqlem  12391  ennnfonelemhf1o  12414  strslssd  12509  ressbas2d  12528  ressinbasd  12533  topnidg  12701  lidrideqd  12800  grpidd  12802  grpridd  12806  ismndd  12838  grpidd2  12914  grpinvid1  12924  grpinvid2  12925  grppnpcan2  12964  grpnpncan  12965  dfgrp3mlem  12968  grpsubpropd2  12975  mhmid  12979  mhmmnd  12980  mulgsubcl  12997  mulgneg  13001  mulgaddcomlem  13006  mulginvinv  13009  mulgdirlem  13014  mulgdir  13015  mulgass  13020  mulgmodid  13022  grpissubg  13054  eqgcpbl  13087  mgptopng  13139  srgisid  13169  ringidss  13212  ringcom  13214  unitgrp  13285  1rinv  13297  0unit  13298  lringuplu  13337  subrgpropd  13369  lmod0vs  13411  lmodvsmmulgdi  13413  lmodvneg1  13420  lmodcom  13423  lmodsubvs  13433  lmodsubdir  13435  lmodpropd  13439  zringmulg  13491  restopnb  13684  txcnmpt  13776  cnmpt1t  13788  blhalf  13911  xmspropd  13980  mspropd  13981  limcimolemlt  14136  dvfre  14177  dveflem  14190  dvef  14191  sin2kpi  14235  cos2kpi  14236  sin2pim  14237  cos2pim  14238  ptolemy  14248  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  tangtx  14262  sincosq1eq  14263  abssinper  14270  sinkpi  14271  relogeftb  14289  relogoprlem  14292  relogexp  14296  lgsval2lem  14414  lgsdir2lem4  14435  lgsdirprm  14438  lgsdilem2  14440  2sqlem4  14468  2sqlem6  14470  2sqlem8  14473  peano3nninf  14759  nninfsel  14769  nninffeq  14772  isomninnlem  14781  cvgcmp2nlemabs  14783  trilpolemlt1  14792  trirec0xor  14796  ismkvnnlem  14803