Theorem eqtr3di 2779

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3di.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3di	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 ⊢ 𝐴 = 𝐶
2	1	eqcomi 2738	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2777	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  resdmdfsn  5991  f0dom0  6726  f1o00  6817  fmpt  7064  fmptsn  7123  fninfp  7130  uniordint  7757  fsuppeq  8131  fsuppeqg  8132  mapsnd  8836  sbthlem4  9031  sbthlem6  9033  findcard2s  9106  ssfi  9114  elfiun  9357  cnfcom2  9631  rankxplim3  9810  rankxpsuc  9811  pm54.43  9930  axdc3lem4  10382  gruun  10735  recmulnq  10893  reclem3pr  10978  xrmineq  13116  xadddi2  13233  iooval2  13315  hashsng  14310  hashfun  14378  hashbc  14394  swrds2m  14883  isumclim3  15701  isummulc2  15704  iprodclim3  15942  bpolydiflem  15996  bpoly4  16001  fprodefsum  16037  ruclem4  16178  bitsshft  16421  phimullem  16725  pythagtriplem1  16763  1arithlem4  16873  fsets  17115  topnid  17374  submefmnd  18798  pgrpsubgsymg  19315  odhash  19480  gsumzf1o  19818  gsumdifsnd  19867  pgpfaclem1  19989  fincygsubgodd  20020  subdrgint  20688  mplcoe1  21920  mplcoe5  21923  evlslem4  21959  ordtrest2  23067  ufildr  23794  tsmsres  24007  zlmclm  24988  cphipval2  25117  csschl  25252  rrxcph  25268  volinun  25423  uniioombllem4  25463  itg1climres  25591  limcco  25770  vieta1lem2  26195  coseq00topi  26387  tangtx  26390  coskpi  26408  advlog  26539  advlogexp  26540  logtayl  26545  logccv  26548  dvcxp1  26625  dvcncxp1  26628  loglesqrt  26647  ang180lem3  26697  dquart  26739  atans2  26817  basellem8  26974  chtub  27099  bposlem6  27176  lgsquadlem2  27268  logdivsum  27420  log2sumbnd  27431  nodenselem5  27576  oldsuc  27773  precsexlem3  28087  zs12bday  28319  spthispth  29627  ipval3  30611  siii  30755  cm2j  31522  pjssmii  31583  opsqrlem1  32042  hmopidmchi  32053  hmopidmpji  32054  pjcmul1i  32103  mddmd2  32211  cvexchlem  32270  dmdbr6ati  32325  difeq  32420  difuncomp  32455  ffsrn  32625  fzo0opth  32701  symgcom2  33014  cycpmcl  33046  cycpm2tr  33049  rhmimaidl  33376  drngidlhash  33378  1arithidomlem2  33480  qusdimsum  33597  2sqr3minply  33743  cos9thpiminplylem2  33746  zarcmplem  33844  ordtprsuni  33882  ordtrest2NEW  33886  zzsnm  33922  measun  34174  sxbrsigalem2  34250  carsgsigalem  34279  eulerpartlemgu  34341  gsumnunsn  34505  signsplypnf  34514  logdivsqrle  34614  cvmlift2lem12  35274  satf0suc  35336  nepss  35678  fwddifnp1  36126  finxpreclem1  37350  finxpreclem3  37354  poimirlem31  37618  ismblfin  37628  dvtan  37637  itg2addnclem3  37640  dvasin  37671  dvacos  37672  dvreasin  37673  dvreacos  37674  areacirclem1  37675  cnvepima  38292  glbconN  39343  glbconNOLD  39344  pmodl42N  39818  2polssN  39882  cdleme20j  40285  trlcocnv  40687  trlcone  40695  lclkrlem2c  41476  readvrec2  42322  sn-00idlem3  42361  sn-mul01  42387  selvvvval  42546  diophrw  42720  wopprc  42992  onuniintrab  43188  fsovcnvlem  43975  sineq0ALT  44899  founiiun0  45157  iccdifioo  45486  itgvol0  45939  fourierdlem33  46111  etransclem32  46237  simpcntrab  46841  cycl3grtrilem  47918  gpg3kgrtriexlem2  48048  gpgprismgr4cycllem3  48060  gsumdifsndf  48142  zlmodzxzadd  48319  cosn  48795  oppcendc  48980  resccatlem  49035  resccat  49036  0funcg2  49046  imaf1hom  49070