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  4239  eusvnf  4455  f00  5409  f1imacnv  5480  foimacnv  5481  f1ococnv1  5492  funfvdm  5582  fvmptdf  5606  fndmdif  5624  acexmidlemph  5871  acexmidlemab  5872  ovmpodf  6009  oprssov  6019  tfrlemisucaccv  6329  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  oav2  6467  omv2  6469  fnsnsplitdc  6509  ecopovtrn  6635  ecopovtrng  6638  map0b  6690  en1  6802  ssenen  6854  fidifsnen  6873  dif1en  6882  undifdc  6926  fidcenumlemr  6957  ordiso2  7037  nnnninfeq2  7130  nninfisollemne  7132  finomni  7141  exmidomni  7143  fodjum  7147  exmidaclem  7210  distrnqg  7389  1qec  7390  prarloclemarch2  7421  nnnq0lem1  7448  nqpnq0nq  7455  distrnq0  7461  prarloclemlt  7495  prmuloclemcalc  7567  ltaprg  7621  prplnqu  7622  recexprlem1ssl  7635  recexprlem1ssu  7636  ltmprr  7644  cauappcvgprlemopl  7648  caucvgprlemopl  7671  caucvgprprlemopl  7699  caucvgprprlemexb  7709  prsrlem1  7744  ltsosr  7766  mulgt0sr  7780  recidpipr  7858  recriota  7892  nntopi  7896  axcaucvglemres  7901  addlid  8099  readdcan  8100  muladd11r  8116  add32r  8120  cnegexlem2  8136  cnegex  8138  pncan2  8167  addsubass  8170  subadd23  8172  addsub12  8173  subid  8179  subid1  8180  npncan  8181  nppcan3  8184  subsub  8190  nppcan2  8191  nnncan2  8197  npncan3  8198  pnpcan  8199  negdi  8217  mvlraddd  8324  mvlladdd  8325  pnpncand  8335  subdi  8345  mulsub  8361  mulsub2  8362  eqord1  8443  recexap  8613  div32ap  8652  divsubdirap  8668  divmuldivap  8672  divdivdivap  8673  divmuleqap  8677  divcanap6  8679  dmdcanap  8682  divsubdivap  8688  div2negap  8695  div2subap  8797  mvllmulapd  8802  prodgt0gt0  8811  cju  8921  zneo  9357  infrenegsupex  9597  qreccl  9645  mul2lt0rlt0  9762  xnpcan  9875  fzosn  10208  modqid  10352  modqm1p1mod0  10378  modqltm1p1mod  10379  modqmul1  10380  modaddmodup  10390  modaddmodlo  10391  modqsubdir  10396  iseqf1olemkle  10487  iseqf1olemklt  10488  seq3f1olemstep  10504  seq3f1oleml  10506  seqfeq3  10515  seq3distr  10516  expineg2  10532  expm1t  10551  expadd  10565  expaddzaplem  10566  expmulzap  10569  sqsubswap  10583  subsq2  10631  binom2sub  10637  binom3  10641  facndiv  10722  bcval5  10746  bcn2p1  10753  bcnm1  10755  2shfti  10843  shftcan2  10847  reim0  10873  imval2  10906  cjreim2  10916  cjdivap  10921  cnrecnv  10922  rennim  11014  resqrexlemnm  11030  remsqsqrt  11044  sqrtdiv  11054  sqrtmsq  11057  sqabsadd  11067  sqabssub  11068  absreim  11080  absdivap  11082  absnid  11085  sqabs  11094  abslt  11100  absle  11101  recvalap  11109  abssub  11113  maxabslemlub  11219  infxrnegsupex  11274  mulcn2  11323  reccn2ap  11324  cjcn2  11327  summodclem3  11391  summodclem2a  11392  summodc  11394  zsumdc  11395  fsum3  11398  fisumss  11403  fsumcl2lem  11409  fsumm1  11427  fsum1p  11429  isummulc2  11437  telfsumo  11477  binomlem  11494  bcxmas  11500  arisum  11509  trireciplem  11511  trirecip  11512  geolim2  11523  georeclim  11524  cvgratnnlemfm  11540  cvgratz  11543  mertenslemi1  11546  clim2divap  11551  prodmodclem3  11586  prodmodclem2a  11587  zproddc  11590  fprodseq  11594  fprodssdc  11601  fprod1p  11610  efcan  11687  efexp  11693  efzval  11694  efgt0  11695  eftlub  11701  efltim  11709  resinval  11726  recosval  11727  cosmul  11756  cos2t  11761  cos2tsin  11762  cos01bnd  11769  cos12dec  11778  eirraplem  11787  muldvds1  11826  dvdsexp  11870  oexpneg  11885  divalglemqt  11927  divalglemeunn  11929  divalglemeuneg  11931  divalgmod  11935  flodddiv4t2lthalf  11945  gcdid0  11984  gcdaddm  11988  dvdsgcdidd  11998  rpmulgcd  12030  sqgcd  12033  algcvg  12051  eucalgcvga  12061  eucalg  12062  dvdslcm  12072  lcmeq0  12074  lcmgcd  12081  qredeu  12100  sqnprm  12139  divgcdodd  12146  sqrt2irrlem  12164  sqpweven  12178  2sqpwodd  12179  divnumden  12199  hashdvds  12224  phimullem  12228  eulerthlemrprm  12232  eulerthlemth  12235  odzdvds  12248  pythagtriplem3  12270  pythagtriplem4  12271  pythagtriplem14  12280  pythagtriplem19  12285  pcpremul  12296  pceulem  12297  pcqdiv  12310  pcaddlem  12341  fldivp1  12349  1arithlem4  12367  4sqlem10  12388  mul4sqlem  12394  ennnfonelemhf1o  12417  strslssd  12512  ressbas2d  12531  ressinbasd  12536  topnidg  12707  lidrideqd  12806  grpidd  12808  grpridd  12812  ismndd  12844  grpidd2  12920  grpinvid1  12930  grpinvid2  12931  grppnpcan2  12970  grpnpncan  12971  dfgrp3mlem  12974  grpsubpropd2  12981  mhmid  12985  mhmmnd  12986  mulgsubcl  13003  mulgneg  13007  mulgaddcomlem  13012  mulginvinv  13015  mulgdirlem  13020  mulgdir  13021  mulgass  13026  mulgmodid  13028  grpissubg  13060  eqgcpbl  13093  mgptopng  13145  srgisid  13175  ringidss  13218  ringcom  13220  unitgrp  13291  1rinv  13303  0unit  13304  lringuplu  13343  subrgpropd  13375  lmod0vs  13417  lmodvsmmulgdi  13419  lmodvneg1  13426  lmodcom  13429  lmodsubvs  13439  lmodsubdir  13441  lmodpropd  13445  lspsnsub  13513  lspsneq0b  13519  lsppropd  13524  lidlbas  13567  zringmulg  13628  restopnb  13821  txcnmpt  13913  cnmpt1t  13925  blhalf  14048  xmspropd  14117  mspropd  14118  limcimolemlt  14273  dvfre  14314  dveflem  14327  dvef  14328  sin2kpi  14372  cos2kpi  14373  sin2pim  14374  cos2pim  14375  ptolemy  14385  sincosq2sgn  14388  sincosq3sgn  14389  sincosq4sgn  14390  sinq12gt0  14391  tangtx  14399  sincosq1eq  14400  abssinper  14407  sinkpi  14408  relogeftb  14426  relogoprlem  14429  relogexp  14433  lgsval2lem  14551  lgsdir2lem4  14572  lgsdirprm  14575  lgsdilem2  14577  2sqlem4  14605  2sqlem6  14607  2sqlem8  14610  peano3nninf  14897  nninfsel  14907  nninffeq  14910  isomninnlem  14919  cvgcmp2nlemabs  14921  trilpolemlt1  14930  trirec0xor  14934  ismkvnnlem  14941