Theorem eqtr3di 2790

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 2744	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2788	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  resdmdfsn  6051  f0dom0  6793  f1o00  6884  fmpt  7130  fmptsn  7187  fninfp  7194  uniordint  7821  fsuppeq  8199  fsuppeqg  8200  mapsnd  8925  sbthlem4  9125  sbthlem6  9127  findcard2s  9204  ssfi  9212  elfiun  9468  cnfcom2  9740  rankxplim3  9919  rankxpsuc  9920  pm54.43  10039  axdc3lem4  10491  gruun  10844  recmulnq  11002  reclem3pr  11087  xrmineq  13219  xadddi2  13336  iooval2  13417  hashsng  14405  hashfun  14473  hashbc  14489  swrds2m  14977  isumclim3  15792  isummulc2  15795  iprodclim3  16033  bpolydiflem  16087  bpoly4  16092  fprodefsum  16128  ruclem4  16267  bitsshft  16509  phimullem  16813  pythagtriplem1  16850  1arithlem4  16960  fsets  17203  topnid  17482  submefmnd  18921  pgrpsubgsymg  19442  odhash  19607  gsumzf1o  19945  gsumdifsnd  19994  pgpfaclem1  20116  fincygsubgodd  20147  subdrgint  20821  mplcoe1  22073  mplcoe5  22076  evlslem4  22118  ordtrest2  23228  ufildr  23955  tsmsres  24168  zlmclm  25159  cphipval2  25289  csschl  25424  rrxcph  25440  volinun  25595  uniioombllem4  25635  itg1climres  25764  limcco  25943  vieta1lem2  26368  coseq00topi  26559  tangtx  26562  coskpi  26580  advlog  26711  advlogexp  26712  logtayl  26717  logccv  26720  dvcxp1  26797  dvcncxp1  26800  loglesqrt  26819  ang180lem3  26869  dquart  26911  atans2  26989  basellem8  27146  chtub  27271  bposlem6  27348  lgsquadlem2  27440  logdivsum  27592  log2sumbnd  27603  nodenselem5  27748  oldsuc  27939  precsexlem3  28248  zs12bday  28439  spthispth  29759  ipval3  30738  siii  30882  cm2j  31649  pjssmii  31710  opsqrlem1  32169  hmopidmchi  32180  hmopidmpji  32181  pjcmul1i  32230  mddmd2  32338  cvexchlem  32397  dmdbr6ati  32452  difeq  32546  difuncomp  32574  ffsrn  32747  fzo0opth  32813  symgcom2  33087  cycpmcl  33119  cycpm2tr  33122  rhmimaidl  33440  drngidlhash  33442  1arithidomlem2  33544  qusdimsum  33656  2sqr3minply  33753  zarcmplem  33842  ordtprsuni  33880  ordtrest2NEW  33884  zzsnm  33920  measun  34192  sxbrsigalem2  34268  carsgsigalem  34297  eulerpartlemgu  34359  gsumnunsn  34535  signsplypnf  34544  logdivsqrle  34644  cvmlift2lem12  35299  satf0suc  35361  nepss  35698  fwddifnp1  36147  finxpreclem1  37372  finxpreclem3  37376  poimirlem31  37638  ismblfin  37648  dvtan  37657  itg2addnclem3  37660  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem1  37695  cnvepima  38319  glbconN  39359  glbconNOLD  39360  pmodl42N  39834  2polssN  39898  cdleme20j  40301  trlcocnv  40703  trlcone  40711  lclkrlem2c  41492  readvrec2  42370  sn-mul01  42432  selvvvval  42572  diophrw  42747  wopprc  43019  onuniintrab  43215  fsovcnvlem  44003  sineq0ALT  44935  founiiun0  45133  iccdifioo  45468  itgvol0  45924  fourierdlem33  46096  etransclem32  46222  simpcntrab  46826  gsumdifsndf  48025  zlmodzxzadd  48203