Theorem eqtr3di 2786

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

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  resdmdfsn  5886  f0dom0  6581  f1o00  6673  fmpt  6905  fmptsn  6960  fninfp  6967  uniordint  7563  frnsuppeq  7895  frnsuppeqg  7896  mapsnd  8545  sbthlem4  8737  sbthlem6  8739  findcard2s  8821  ssfi  8829  elfiun  9024  cnfcom2  9295  rankxplim3  9462  rankxpsuc  9463  pm54.43  9582  axdc3lem4  10032  gruun  10385  recmulnq  10543  reclem3pr  10628  xrmineq  12735  xadddi2  12852  iooval2  12933  hashsng  13901  hashfun  13969  hashbc  13982  swrds2m  14471  isumclim3  15286  isummulc2  15289  iprodclim3  15525  bpolydiflem  15579  bpoly4  15584  fprodefsum  15619  ruclem4  15758  bitsshft  15997  phimullem  16295  pythagtriplem1  16332  1arithlem4  16442  fsets  16698  topnid  16894  submefmnd  18276  pgrpsubgsymg  18755  odhash  18917  gsumzf1o  19251  gsumdifsnd  19300  pgpfaclem1  19422  fincygsubgodd  19453  subdrgint  19801  mplcoe1  20948  mplcoe5  20951  evlslem4  20988  ordtrest2  22055  ufildr  22782  tsmsres  22995  zlmclm  23963  cphipval2  24092  csschl  24227  rrxcph  24243  volinun  24397  uniioombllem4  24437  itg1climres  24566  limcco  24744  vieta1lem2  25158  coseq00topi  25346  tangtx  25349  coskpi  25366  advlog  25496  advlogexp  25497  logtayl  25502  logccv  25505  dvcxp1  25580  dvcncxp1  25583  loglesqrt  25598  ang180lem3  25648  dquart  25690  atans2  25768  basellem8  25924  chtub  26047  bposlem6  26124  lgsquadlem2  26216  logdivsum  26368  log2sumbnd  26379  spthispth  27767  ipval3  28744  siii  28888  cm2j  29655  pjssmii  29716  opsqrlem1  30175  hmopidmchi  30186  hmopidmpji  30187  pjcmul1i  30236  mddmd2  30344  cvexchlem  30403  dmdbr6ati  30458  difeq  30538  difuncomp  30566  ffsrn  30738  symgcom2  31026  cycpmcl  31056  cycpm2tr  31059  rhmimaidl  31277  qusdimsum  31377  zarcmplem  31499  ordtprsuni  31537  ordtrest2NEW  31541  zzsnm  31577  measun  31845  sxbrsigalem2  31919  carsgsigalem  31948  eulerpartlemgu  32010  gsumnunsn  32186  signsplypnf  32195  logdivsqrle  32296  cvmlift2lem12  32943  satf0suc  33005  nepss  33331  nodenselem5  33577  oldsuc  33754  fwddifnp1  34153  finxpreclem1  35246  finxpreclem3  35250  poimirlem31  35494  ismblfin  35504  dvtan  35513  itg2addnclem3  35516  dvasin  35547  dvacos  35548  dvreasin  35549  dvreacos  35550  areacirclem1  35551  cnvepima  36158  glbconN  37077  pmodl42N  37551  2polssN  37615  cdleme20j  38018  trlcocnv  38420  trlcone  38428  lclkrlem2c  39209  sn-mul01  40056  diophrw  40225  wopprc  40496  fsovcnvlem  41239  sineq0ALT  42171  founiiun0  42342  iccdifioo  42669  itgvol0  43127  fourierdlem33  43299  etransclem32  43425  simpcntrab  44001  gsumdifsndf  44991  zlmodzxzadd  45310