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  6002  f0dom0  6744  f1o00  6835  fmpt  7082  fmptsn  7141  fninfp  7148  uniordint  7777  fsuppeq  8154  fsuppeqg  8155  mapsnd  8859  sbthlem4  9054  sbthlem6  9056  findcard2s  9129  ssfi  9137  elfiun  9381  cnfcom2  9655  rankxplim3  9834  rankxpsuc  9835  pm54.43  9954  axdc3lem4  10406  gruun  10759  recmulnq  10917  reclem3pr  11002  xrmineq  13140  xadddi2  13257  iooval2  13339  hashsng  14334  hashfun  14402  hashbc  14418  swrds2m  14907  isumclim3  15725  isummulc2  15728  iprodclim3  15966  bpolydiflem  16020  bpoly4  16025  fprodefsum  16061  ruclem4  16202  bitsshft  16445  phimullem  16749  pythagtriplem1  16787  1arithlem4  16897  fsets  17139  topnid  17398  submefmnd  18822  pgrpsubgsymg  19339  odhash  19504  gsumzf1o  19842  gsumdifsnd  19891  pgpfaclem1  20013  fincygsubgodd  20044  subdrgint  20712  mplcoe1  21944  mplcoe5  21947  evlslem4  21983  ordtrest2  23091  ufildr  23818  tsmsres  24031  zlmclm  25012  cphipval2  25141  csschl  25276  rrxcph  25292  volinun  25447  uniioombllem4  25487  itg1climres  25615  limcco  25794  vieta1lem2  26219  coseq00topi  26411  tangtx  26414  coskpi  26432  advlog  26563  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  dvcncxp1  26652  loglesqrt  26671  ang180lem3  26721  dquart  26763  atans2  26841  basellem8  26998  chtub  27123  bposlem6  27200  lgsquadlem2  27292  logdivsum  27444  log2sumbnd  27455  nodenselem5  27600  oldsuc  27797  precsexlem3  28111  zs12bday  28343  spthispth  29654  ipval3  30638  siii  30782  cm2j  31549  pjssmii  31610  opsqrlem1  32069  hmopidmchi  32080  hmopidmpji  32081  pjcmul1i  32130  mddmd2  32238  cvexchlem  32297  dmdbr6ati  32352  difeq  32447  difuncomp  32482  ffsrn  32652  fzo0opth  32728  symgcom2  33041  cycpmcl  33073  cycpm2tr  33076  rhmimaidl  33403  drngidlhash  33405  1arithidomlem2  33507  qusdimsum  33624  2sqr3minply  33770  cos9thpiminplylem2  33773  zarcmplem  33871  ordtprsuni  33909  ordtrest2NEW  33913  zzsnm  33949  measun  34201  sxbrsigalem2  34277  carsgsigalem  34306  eulerpartlemgu  34368  gsumnunsn  34532  signsplypnf  34541  logdivsqrle  34641  cvmlift2lem12  35301  satf0suc  35363  nepss  35705  fwddifnp1  36153  finxpreclem1  37377  finxpreclem3  37381  poimirlem31  37645  ismblfin  37655  dvtan  37664  itg2addnclem3  37667  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  areacirclem1  37702  cnvepima  38319  glbconN  39370  glbconNOLD  39371  pmodl42N  39845  2polssN  39909  cdleme20j  40312  trlcocnv  40714  trlcone  40722  lclkrlem2c  41503  readvrec2  42349  sn-00idlem3  42388  sn-mul01  42414  selvvvval  42573  diophrw  42747  wopprc  43019  onuniintrab  43215  fsovcnvlem  44002  sineq0ALT  44926  founiiun0  45184  iccdifioo  45513  itgvol0  45966  fourierdlem33  46138  etransclem32  46264  simpcntrab  46868  cycl3grtrilem  47945  gpg3kgrtriexlem2  48075  gpgprismgr4cycllem3  48087  gsumdifsndf  48169  zlmodzxzadd  48346  cosn  48822  oppcendc  49007  resccatlem  49062  resccat  49063  0funcg2  49073  imaf1hom  49097