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  5982  f0dom0  6708  f1o00  6799  fmpt  7044  fmptsn  7103  fninfp  7110  uniordint  7737  fsuppeq  8108  fsuppeqg  8109  mapsnd  8813  sbthlem4  9007  sbthlem6  9009  findcard2s  9079  ssfi  9087  elfiun  9320  cnfcom2  9598  rankxplim3  9777  rankxpsuc  9778  pm54.43  9897  axdc3lem4  10347  gruun  10700  recmulnq  10858  reclem3pr  10943  xrmineq  13082  xadddi2  13199  iooval2  13281  hashsng  14276  hashfun  14344  hashbc  14360  swrds2m  14848  isumclim3  15666  isummulc2  15669  iprodclim3  15907  bpolydiflem  15961  bpoly4  15966  fprodefsum  16002  ruclem4  16143  bitsshft  16386  phimullem  16690  pythagtriplem1  16728  1arithlem4  16838  fsets  17080  topnid  17339  submefmnd  18769  pgrpsubgsymg  19288  odhash  19453  gsumzf1o  19791  gsumdifsnd  19840  pgpfaclem1  19962  fincygsubgodd  19993  subdrgint  20688  mplcoe1  21942  mplcoe5  21945  evlslem4  21981  ordtrest2  23089  ufildr  23816  tsmsres  24029  zlmclm  25010  cphipval2  25139  csschl  25274  rrxcph  25290  volinun  25445  uniioombllem4  25485  itg1climres  25613  limcco  25792  vieta1lem2  26217  coseq00topi  26409  tangtx  26412  coskpi  26430  advlog  26561  advlogexp  26562  logtayl  26567  logccv  26570  dvcxp1  26647  dvcncxp1  26650  loglesqrt  26669  ang180lem3  26719  dquart  26761  atans2  26839  basellem8  26996  chtub  27121  bposlem6  27198  lgsquadlem2  27290  logdivsum  27442  log2sumbnd  27453  nodenselem5  27598  oldsuc  27800  precsexlem3  28116  zs12bday  28361  spthispth  29669  ipval3  30653  siii  30797  cm2j  31564  pjssmii  31625  opsqrlem1  32084  hmopidmchi  32095  hmopidmpji  32096  pjcmul1i  32145  mddmd2  32253  cvexchlem  32312  dmdbr6ati  32367  difeq  32462  difuncomp  32497  ffsrn  32672  fzo0opth  32748  symgcom2  33026  cycpmcl  33058  cycpm2tr  33061  rhmimaidl  33369  drngidlhash  33371  1arithidomlem2  33473  qusdimsum  33595  2sqr3minply  33747  cos9thpiminplylem2  33750  zarcmplem  33848  ordtprsuni  33886  ordtrest2NEW  33890  zzsnm  33926  measun  34178  sxbrsigalem2  34254  carsgsigalem  34283  eulerpartlemgu  34345  gsumnunsn  34509  signsplypnf  34518  logdivsqrle  34618  cvmlift2lem12  35287  satf0suc  35349  nepss  35691  fwddifnp1  36139  finxpreclem1  37363  finxpreclem3  37367  poimirlem31  37631  ismblfin  37641  dvtan  37650  itg2addnclem3  37653  dvasin  37684  dvacos  37685  dvreasin  37686  dvreacos  37687  areacirclem1  37688  cnvepima  38305  glbconN  39356  pmodl42N  39830  2polssN  39894  cdleme20j  40297  trlcocnv  40699  trlcone  40707  lclkrlem2c  41488  readvrec2  42334  sn-00idlem3  42373  sn-mul01  42399  selvvvval  42558  diophrw  42732  wopprc  43003  onuniintrab  43199  fsovcnvlem  43986  sineq0ALT  44910  founiiun0  45168  iccdifioo  45496  itgvol0  45949  fourierdlem33  46121  etransclem32  46247  simpcntrab  46851  cycl3grtrilem  47930  gpg3kgrtriexlem2  48068  gpgprismgr4cycllem3  48081  gsumdifsndf  48165  zlmodzxzadd  48342  cosn  48818  oppcendc  49003  resccatlem  49058  resccat  49059  0funcg2  49069  imaf1hom  49093