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  18804  pgrpsubgsymg  19323  odhash  19488  gsumzf1o  19826  gsumdifsnd  19875  pgpfaclem1  19997  fincygsubgodd  20028  subdrgint  20723  mplcoe1  21977  mplcoe5  21980  evlslem4  22016  ordtrest2  23124  ufildr  23851  tsmsres  24064  zlmclm  25045  cphipval2  25174  csschl  25309  rrxcph  25325  volinun  25480  uniioombllem4  25520  itg1climres  25648  limcco  25827  vieta1lem2  26252  coseq00topi  26444  tangtx  26447  coskpi  26465  advlog  26596  advlogexp  26597  logtayl  26602  logccv  26605  dvcxp1  26682  dvcncxp1  26685  loglesqrt  26704  ang180lem3  26754  dquart  26796  atans2  26874  basellem8  27031  chtub  27156  bposlem6  27233  lgsquadlem2  27325  logdivsum  27477  log2sumbnd  27488  nodenselem5  27633  oldsuc  27835  precsexlem3  28151  zs12bday  28396  spthispth  29704  ipval3  30688  siii  30832  cm2j  31599  pjssmii  31660  opsqrlem1  32119  hmopidmchi  32130  hmopidmpji  32131  pjcmul1i  32180  mddmd2  32288  cvexchlem  32347  dmdbr6ati  32402  difeq  32497  difuncomp  32532  ffsrn  32702  fzo0opth  32778  symgcom2  33056  cycpmcl  33088  cycpm2tr  33091  rhmimaidl  33396  drngidlhash  33398  1arithidomlem2  33500  qusdimsum  33617  2sqr3minply  33763  cos9thpiminplylem2  33766  zarcmplem  33864  ordtprsuni  33902  ordtrest2NEW  33906  zzsnm  33942  measun  34194  sxbrsigalem2  34270  carsgsigalem  34299  eulerpartlemgu  34361  gsumnunsn  34525  signsplypnf  34534  logdivsqrle  34634  cvmlift2lem12  35294  satf0suc  35356  nepss  35698  fwddifnp1  36146  finxpreclem1  37370  finxpreclem3  37374  poimirlem31  37638  ismblfin  37648  dvtan  37657  itg2addnclem3  37660  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem1  37695  cnvepima  38312  glbconN  39363  glbconNOLD  39364  pmodl42N  39838  2polssN  39902  cdleme20j  40305  trlcocnv  40707  trlcone  40715  lclkrlem2c  41496  readvrec2  42342  sn-00idlem3  42381  sn-mul01  42407  selvvvval  42566  diophrw  42740  wopprc  43012  onuniintrab  43208  fsovcnvlem  43995  sineq0ALT  44919  founiiun0  45177  iccdifioo  45506  itgvol0  45959  fourierdlem33  46131  etransclem32  46257  simpcntrab  46861  cycl3grtrilem  47938  gpg3kgrtriexlem2  48068  gpgprismgr4cycllem3  48080  gsumdifsndf  48162  zlmodzxzadd  48339  cosn  48815  oppcendc  49000  resccatlem  49055  resccat  49056  0funcg2  49066  imaf1hom  49090