Theorem eqtr3di 2819

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  resdmdfsnOLD  6033  f0dom0  6763  f1o00  6857  fmpt  7106  fmptsn  7166  fninfp  7173  uniordint  7799  fsuppeq  8170  fsuppeqg  8171  mapsnd  8883  sbthlem4  9077  sbthlem6  9079  findcard2s  9149  ssfi  9156  elfiun  9389  cnfcom2  9670  rankxplim3  9852  rankxpsuc  9853  pm54.43  9986  axdc3lem4  10436  gruun  10790  recmulnq  10948  reclem3pr  11033  xrmineq  13205  xadddi2  13322  iooval2  13404  hashsng  14404  hashfun  14473  hashbc  14489  swrds2m  14977  isumclim3  15809  isummulc2  15812  iprodclim3  16053  bpolydiflem  16107  bpoly4  16112  fprodefsum  16148  ruclem4  16289  bitsshft  16532  phimullem  16837  pythagtriplem1  16875  1arithlem4  16985  fsets  17228  topnid  17487  submefmnd  18953  pgrpsubgsymg  19478  odhash  19643  gsumzf1o  19981  gsumdifsnd  20030  pgpfaclem1  20152  fincygsubgodd  20183  subdrgint  20883  mplcoe1  22156  mplcoe5  22159  evlslem4  22195  selvvvval  22261  ordtrest2  23329  ufildr  24056  tsmsres  24269  zlmclm  25239  cphipval2  25368  csschl  25503  rrxcph  25519  volinun  25673  uniioombllem4  25713  itg1climres  25841  limcco  26020  vieta1lem2  26440  coseq00topi  26632  tangtx  26635  coskpi  26653  advlog  26784  advlogexp  26785  logtayl  26790  logccv  26793  dvcxp1  26870  dvcncxp1  26873  loglesqrt  26891  ang180lem3  26941  dquart  26983  atans2  27061  basellem8  27217  chtub  27341  bposlem6  27418  lgsquadlem2  27510  logdivsum  27662  log2sumbnd  27673  nodenselem5  27817  oldsuc  28044  precsexlem3  28367  spthispth  30013  ipval3  31001  siii  31145  cm2j  31912  pjssmii  31973  opsqrlem1  32432  hmopidmchi  32443  hmopidmpji  32444  pjcmul1i  32493  mddmd2  32601  cvexchlem  32660  dmdbr6ati  32715  difeq  32804  difuncomp  32838  ffsrn  33013  fzo0opth  33088  symgcom2  33344  cycpmcl  33376  cycpm2tr  33379  rhmimaidl  33683  drngidlhash  33685  1arithidomlem2  33770  qusdimsum  33962  2sqr3minply  34114  cos9thpiminplylem2  34117  zarcmplem  34215  ordtprsuni  34253  ordtrest2NEW  34257  zzsnm  34293  measun  34545  sxbrsigalem2  34620  carsgsigalem  34649  eulerpartlemgu  34711  gsumnunsn  34875  signsplypnf  34881  logdivsqrle  34981  cvmlift2lem12  35704  satf0suc  35766  nepss  36108  fwddifnp1  36555  finxpreclem1  37922  finxpreclem3  37926  poimirlem3  38161  poimirlem31  38189  ismblfin  38199  dvtan  38208  itg2addnclem3  38211  dvasin  38242  dvacos  38243  dvreasin  38244  dvreacos  38245  areacirclem1  38246  cnvepima  38875  disjimeceqim  39342  glbconN  40040  pmodl42N  40514  2polssN  40578  cdleme20j  40981  trlcocnv  41383  trlcone  41391  lclkrlem2c  42172  readvrec2  43011  sn-00idlem3  43050  sn-mul01  43076  diophrw  43381  wopprc  43648  onuniintrab  43844  fsovcnvlem  44630  sineq0ALT  45536  founiiun0  45799  iccdifioo  46122  itgvol0  46573  fourierdlem33  46745  etransclem32  46871  simpcntrab  47475  chnsubseqwl  47486  sin5tlem1  47498  cycl3grtrilem  48599  gpg3kgrtriexlem2  48737  gpgprismgr4cycllem3  48750  gsumdifsndf  48834  zlmodzxzadd  49022  cosn  49496  oppcendc  49680  resccatlem  49735  resccat  49736  0funcg2  49746  imaf1hom  49770