Theorem eqtr3d 2264

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3d  2270  3eqtr3rd  2271  3eqtr3a  2286  opth  4324  eusvnf  4545  f00  5522  f1imacnv  5594  foimacnv  5595  f1ococnv1  5606  funfvdm  5702  fvmptdf  5727  fndmdif  5745  funopsn  5822  acexmidlemph  6003  acexmidlemab  6004  ovmpodf  6145  fvmpopr2d  6150  oprssov  6156  tfrlemisucaccv  6482  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  oav2  6622  omv2  6624  fnsnsplitdc  6664  ecopovtrn  6792  ecopovtrng  6795  map0b  6847  en1  6964  ssenen  7025  fidifsnen  7045  dif1en  7054  undifdc  7102  fidcenumlemr  7138  ordiso2  7218  nninfninc  7306  nnnninfeq2  7312  nninfisollemne  7314  finomni  7323  exmidomni  7325  fodjum  7329  exmidaclem  7406  distrnqg  7590  1qec  7591  prarloclemarch2  7622  nnnq0lem1  7649  nqpnq0nq  7656  distrnq0  7662  prarloclemlt  7696  prmuloclemcalc  7768  ltaprg  7822  prplnqu  7823  recexprlem1ssl  7836  recexprlem1ssu  7837  ltmprr  7845  cauappcvgprlemopl  7849  caucvgprlemopl  7872  caucvgprprlemopl  7900  caucvgprprlemexb  7910  prsrlem1  7945  ltsosr  7967  mulgt0sr  7981  recidpipr  8059  recriota  8093  nntopi  8097  axcaucvglemres  8102  addlid  8301  readdcan  8302  muladd11r  8318  add32r  8322  cnegexlem2  8338  cnegex  8340  pncan2  8369  addsubass  8372  subadd23  8374  addsub12  8375  subid  8381  subid1  8382  npncan  8383  nppcan3  8386  subsub  8392  nppcan2  8393  nnncan2  8399  npncan3  8400  pnpcan  8401  negdi  8419  mvlraddd  8526  mvlladdd  8527  pnpncand  8537  subdi  8547  mulsub  8563  mulsub2  8564  eqord1  8646  recexap  8816  div32ap  8855  divsubdirap  8871  divmuldivap  8875  divdivdivap  8876  divmuleqap  8880  divcanap6  8882  dmdcanap  8885  divsubdivap  8891  div2negap  8898  div2subap  9000  mvllmulapd  9005  prodgt0gt0  9014  cju  9124  zneo  9564  infrenegsupex  9806  qreccl  9854  mul2lt0rlt0  9972  xnpcan  10085  fzosn  10428  modqid  10588  modqm1p1mod0  10614  modqltm1p1mod  10615  modqmul1  10616  modaddmodup  10626  modaddmodlo  10627  modqsubdir  10632  iseqf1olemkle  10736  iseqf1olemklt  10737  seq3f1olemstep  10753  seq3f1oleml  10755  seqf1oglem2  10759  seqfeq3  10768  seq3distr  10771  expineg2  10787  expm1t  10806  expadd  10820  expaddzaplem  10821  expmulzap  10824  sqsubswap  10838  subsq2  10886  binom2sub  10892  binom3  10896  facndiv  10978  bcval5  11002  bcn2p1  11009  bcnm1  11011  pfxccatpfx2  11290  2shfti  11363  shftcan2  11367  reim0  11393  imval2  11426  cjreim2  11436  cjdivap  11441  cnrecnv  11442  rennim  11534  resqrexlemnm  11550  remsqsqrt  11564  sqrtdiv  11574  sqrtmsq  11577  sqabsadd  11587  sqabssub  11588  absreim  11600  absdivap  11602  absnid  11605  sqabs  11614  abslt  11620  absle  11621  recvalap  11629  abssub  11633  maxabslemlub  11739  infxrnegsupex  11795  mulcn2  11844  reccn2ap  11845  cjcn2  11848  summodclem3  11912  summodclem2a  11913  summodc  11915  zsumdc  11916  fsum3  11919  fisumss  11924  fsumcl2lem  11930  fsumm1  11948  fsum1p  11950  isummulc2  11958  telfsumo  11998  binomlem  12015  bcxmas  12021  arisum  12030  trireciplem  12032  trirecip  12033  geolim2  12044  georeclim  12045  cvgratnnlemfm  12061  cvgratz  12064  mertenslemi1  12067  clim2divap  12072  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  fprodssdc  12122  fprod1p  12131  efcan  12208  efexp  12214  efzval  12215  efgt0  12216  eftlub  12222  efltim  12230  resinval  12247  recosval  12248  cosmul  12277  cos2t  12282  cos2tsin  12283  cos01bnd  12290  cos12dec  12300  eirraplem  12309  muldvds1  12348  dvdsexp  12393  oexpneg  12409  divalglemqt  12451  divalglemeunn  12453  divalglemeuneg  12455  divalgmod  12459  flodddiv4t2lthalf  12471  bitsmod  12488  bitsinv1lem  12493  gcdid0  12522  gcdaddm  12526  dvdsgcdidd  12536  rpmulgcd  12568  sqgcd  12571  algcvg  12591  eucalgcvga  12601  eucalg  12602  dvdslcm  12612  lcmeq0  12614  lcmgcd  12621  qredeu  12640  sqnprm  12679  divgcdodd  12686  sqrt2irrlem  12704  sqpweven  12718  2sqpwodd  12719  divnumden  12739  hashdvds  12764  phimullem  12768  eulerthlemrprm  12772  eulerthlemth  12775  odzdvds  12789  pythagtriplem3  12811  pythagtriplem4  12812  pythagtriplem14  12821  pythagtriplem19  12826  pcpremul  12837  pceulem  12838  pcqdiv  12851  pcaddlem  12883  fldivp1  12892  1arithlem4  12910  4sqlem10  12931  mul4sqlem  12937  4sqlem11  12945  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  ennnfonelemhf1o  13005  strslssd  13100  ressbas2d  13122  ressinbasd  13128  topnidg  13306  lidrideqd  13435  grpidd  13437  grprida  13441  gsumress  13449  ismndd  13491  grpidd2  13595  grpinvid1  13606  grpinvid2  13607  grppnpcan2  13648  grpnpncan  13649  dfgrp3mlem  13652  grpsubpropd2  13659  mhmid  13673  mhmmnd  13674  mulgsubcl  13694  mulgneg  13698  mulgaddcomlem  13703  mulginvinv  13706  mulgdirlem  13711  mulgdir  13712  mulgass  13717  mulgmodid  13719  grpissubg  13752  eqgcpbl  13786  ghmid  13807  ghmmulg  13814  resghm  13818  invghm  13887  gsumfzmptfidmadd  13897  mgptopng  13913  srgisid  13970  ringidss  14013  ringcom  14015  opprsubgg  14068  unitgrp  14101  1rinv  14113  0unit  14114  rhmdvdsr  14160  lringuplu  14181  subrngpropd  14201  subrgpropd  14238  lmod0vs  14306  lmodvsmmulgdi  14308  lmodvneg1  14315  lmodcom  14318  lmodsubvs  14328  lmodsubdir  14330  lmodpropd  14334  lspsnsub  14406  lspsneq0b  14412  lsppropd  14417  rlmscabas  14445  lidlbas  14463  zringmulg  14583  restopnb  14876  txcnmpt  14968  cnmpt1t  14980  blhalf  15103  xmspropd  15172  mspropd  15173  mpomulcn  15261  ivthreinc  15340  limcimolemlt  15359  dvfre  15405  dveflem  15421  dvef  15422  ply1termlem  15437  plymullem1  15443  sin2kpi  15506  cos2kpi  15507  sin2pim  15508  cos2pim  15509  ptolemy  15519  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  tangtx  15533  sincosq1eq  15534  abssinper  15541  sinkpi  15542  relogeftb  15560  relogoprlem  15563  relogexp  15567  mpodvdsmulf1o  15685  mersenne  15692  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgsval2lem  15710  lgsdir2lem4  15731  lgsdirprm  15734  lgsdilem2  15736  gausslemma2dlem7  15768  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem1  15781  lgsquad2lem2  15782  2sqlem4  15818  2sqlem6  15820  2sqlem8  15823  peano3nninf  16487  nninfsel  16497  nninffeq  16500  isomninnlem  16512  cvgcmp2nlemabs  16514  trilpolemlt1  16523  trirec0xor  16527  ismkvnnlem  16534