Theorem eqtr3d 2205

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  3eqtr3d  2211  3eqtr3rd  2212  3eqtr3a  2227  opth  4220  eusvnf  4436  f00  5387  f1imacnv  5457  foimacnv  5458  f1ococnv1  5469  funfvdm  5557  fvmptdf  5581  fndmdif  5599  acexmidlemph  5844  acexmidlemab  5845  ovmpodf  5982  oprssov  5992  tfrlemisucaccv  6302  tfr1onlemsucaccv  6318  tfrcllemsucaccv  6331  oav2  6440  omv2  6442  fnsnsplitdc  6482  ecopovtrn  6608  ecopovtrng  6611  map0b  6663  en1  6775  ssenen  6827  fidifsnen  6846  dif1en  6855  undifdc  6899  fidcenumlemr  6930  ordiso2  7010  nnnninfeq2  7103  nninfisollemne  7105  finomni  7114  exmidomni  7116  fodjum  7120  exmidaclem  7178  distrnqg  7342  1qec  7343  prarloclemarch2  7374  nnnq0lem1  7401  nqpnq0nq  7408  distrnq0  7414  prarloclemlt  7448  prmuloclemcalc  7520  ltaprg  7574  prplnqu  7575  recexprlem1ssl  7588  recexprlem1ssu  7589  ltmprr  7597  cauappcvgprlemopl  7601  caucvgprlemopl  7624  caucvgprprlemopl  7652  caucvgprprlemexb  7662  prsrlem1  7697  ltsosr  7719  mulgt0sr  7733  recidpipr  7811  recriota  7845  nntopi  7849  axcaucvglemres  7854  addid2  8051  readdcan  8052  muladd11r  8068  add32r  8072  cnegexlem2  8088  cnegex  8090  pncan2  8119  addsubass  8122  subadd23  8124  addsub12  8125  subid  8131  subid1  8132  npncan  8133  nppcan3  8136  subsub  8142  nppcan2  8143  nnncan2  8149  npncan3  8150  pnpcan  8151  negdi  8169  mvlraddd  8276  mvlladdd  8277  pnpncand  8287  subdi  8297  mulsub  8313  mulsub2  8314  eqord1  8395  recexap  8564  div32ap  8602  divsubdirap  8618  divmuldivap  8622  divdivdivap  8623  divmuleqap  8627  divcanap6  8629  dmdcanap  8632  divsubdivap  8638  div2negap  8645  div2subap  8747  mvllmulapd  8752  prodgt0gt0  8760  cju  8870  zneo  9306  infrenegsupex  9546  qreccl  9594  mul2lt0rlt0  9709  xnpcan  9822  fzosn  10154  modqid  10298  modqm1p1mod0  10324  modqltm1p1mod  10325  modqmul1  10326  modaddmodup  10336  modaddmodlo  10337  modqsubdir  10342  iseqf1olemkle  10433  iseqf1olemklt  10434  seq3f1olemstep  10450  seq3f1oleml  10452  seqfeq3  10461  seq3distr  10462  expineg2  10478  expm1t  10497  expadd  10511  expaddzaplem  10512  expmulzap  10515  sqsubswap  10529  subsq2  10576  binom2sub  10582  binom3  10586  facndiv  10666  bcval5  10690  bcn2p1  10697  bcnm1  10699  2shfti  10788  shftcan2  10792  reim0  10818  imval2  10851  cjreim2  10861  cjdivap  10866  cnrecnv  10867  rennim  10959  resqrexlemnm  10975  remsqsqrt  10989  sqrtdiv  10999  sqrtmsq  11002  sqabsadd  11012  sqabssub  11013  absreim  11025  absdivap  11027  absnid  11030  sqabs  11039  abslt  11045  absle  11046  recvalap  11054  abssub  11058  maxabslemlub  11164  infxrnegsupex  11219  mulcn2  11268  reccn2ap  11269  cjcn2  11272  summodclem3  11336  summodclem2a  11337  summodc  11339  zsumdc  11340  fsum3  11343  fisumss  11348  fsumcl2lem  11354  fsumm1  11372  fsum1p  11374  isummulc2  11382  telfsumo  11422  binomlem  11439  bcxmas  11445  arisum  11454  trireciplem  11456  trirecip  11457  geolim2  11468  georeclim  11469  cvgratnnlemfm  11485  cvgratz  11488  mertenslemi1  11491  clim2divap  11496  prodmodclem3  11531  prodmodclem2a  11532  zproddc  11535  fprodseq  11539  fprodssdc  11546  fprod1p  11555  efcan  11632  efexp  11638  efzval  11639  efgt0  11640  eftlub  11646  efltim  11654  resinval  11671  recosval  11672  cosmul  11701  cos2t  11706  cos2tsin  11707  cos01bnd  11714  cos12dec  11723  eirraplem  11732  muldvds1  11771  dvdsexp  11814  oexpneg  11829  divalglemqt  11871  divalglemeunn  11873  divalglemeuneg  11875  divalgmod  11879  flodddiv4t2lthalf  11889  gcdid0  11928  gcdaddm  11932  dvdsgcdidd  11942  rpmulgcd  11974  sqgcd  11977  algcvg  11995  eucalgcvga  12005  eucalg  12006  dvdslcm  12016  lcmeq0  12018  lcmgcd  12025  qredeu  12044  sqnprm  12083  divgcdodd  12090  sqrt2irrlem  12108  sqpweven  12122  2sqpwodd  12123  divnumden  12143  hashdvds  12168  phimullem  12172  eulerthlemrprm  12176  eulerthlemth  12179  odzdvds  12192  pythagtriplem3  12214  pythagtriplem4  12215  pythagtriplem14  12224  pythagtriplem19  12229  pcpremul  12240  pceulem  12241  pcqdiv  12254  pcaddlem  12285  fldivp1  12293  1arithlem4  12311  4sqlem10  12332  mul4sqlem  12338  ennnfonelemhf1o  12361  strslssd  12455  topnidg  12585  lidrideqd  12628  grpidd  12630  grpridd  12634  ismndd  12666  grpidd2  12737  restopnb  12940  txcnmpt  13032  cnmpt1t  13044  blhalf  13167  xmspropd  13236  mspropd  13237  limcimolemlt  13392  dvfre  13433  dveflem  13446  dvef  13447  sin2kpi  13491  cos2kpi  13492  sin2pim  13493  cos2pim  13494  ptolemy  13504  sincosq2sgn  13507  sincosq3sgn  13508  sincosq4sgn  13509  sinq12gt0  13510  tangtx  13518  sincosq1eq  13519  abssinper  13526  sinkpi  13527  relogeftb  13545  relogoprlem  13548  relogexp  13552  lgsval2lem  13670  lgsdir2lem4  13691  lgsdirprm  13694  lgsdilem2  13696  2sqlem4  13713  2sqlem6  13715  2sqlem8  13718  peano3nninf  14005  nninfsel  14015  nninffeq  14018  isomninnlem  14027  cvgcmp2nlemabs  14029  trilpolemlt1  14038  trirec0xor  14042  ismkvnnlem  14049