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 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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728

This theorem is referenced by:  resdmdfsn  6023  f0dom0  6767  f1o00  6858  fmpt  7105  fmptsn  7164  fninfp  7171  uniordint  7800  fsuppeq  8179  fsuppeqg  8180  mapsnd  8905  sbthlem4  9105  sbthlem6  9107  findcard2s  9184  ssfi  9192  elfiun  9447  cnfcom2  9721  rankxplim3  9900  rankxpsuc  9901  pm54.43  10020  axdc3lem4  10472  gruun  10825  recmulnq  10983  reclem3pr  11068  xrmineq  13201  xadddi2  13318  iooval2  13400  hashsng  14392  hashfun  14460  hashbc  14476  swrds2m  14965  isumclim3  15780  isummulc2  15783  iprodclim3  16021  bpolydiflem  16075  bpoly4  16080  fprodefsum  16116  ruclem4  16257  bitsshft  16499  phimullem  16803  pythagtriplem1  16841  1arithlem4  16951  fsets  17193  topnid  17454  submefmnd  18878  pgrpsubgsymg  19395  odhash  19560  gsumzf1o  19898  gsumdifsnd  19947  pgpfaclem1  20069  fincygsubgodd  20100  subdrgint  20768  mplcoe1  22000  mplcoe5  22003  evlslem4  22039  ordtrest2  23147  ufildr  23874  tsmsres  24087  zlmclm  25068  cphipval2  25198  csschl  25333  rrxcph  25349  volinun  25504  uniioombllem4  25544  itg1climres  25672  limcco  25851  vieta1lem2  26276  coseq00topi  26468  tangtx  26471  coskpi  26489  advlog  26620  advlogexp  26621  logtayl  26626  logccv  26629  dvcxp1  26706  dvcncxp1  26709  loglesqrt  26728  ang180lem3  26778  dquart  26820  atans2  26898  basellem8  27055  chtub  27180  bposlem6  27257  lgsquadlem2  27349  logdivsum  27501  log2sumbnd  27512  nodenselem5  27657  oldsuc  27854  precsexlem3  28168  zs12bday  28400  spthispth  29711  ipval3  30695  siii  30839  cm2j  31606  pjssmii  31667  opsqrlem1  32126  hmopidmchi  32137  hmopidmpji  32138  pjcmul1i  32187  mddmd2  32295  cvexchlem  32354  dmdbr6ati  32409  difeq  32504  difuncomp  32539  ffsrn  32711  fzo0opth  32787  symgcom2  33100  cycpmcl  33132  cycpm2tr  33135  rhmimaidl  33452  drngidlhash  33454  1arithidomlem2  33556  qusdimsum  33673  2sqr3minply  33819  cos9thpiminplylem2  33822  zarcmplem  33917  ordtprsuni  33955  ordtrest2NEW  33959  zzsnm  33995  measun  34247  sxbrsigalem2  34323  carsgsigalem  34352  eulerpartlemgu  34414  gsumnunsn  34578  signsplypnf  34587  logdivsqrle  34687  cvmlift2lem12  35341  satf0suc  35403  nepss  35740  fwddifnp1  36188  finxpreclem1  37412  finxpreclem3  37416  poimirlem31  37680  ismblfin  37690  dvtan  37699  itg2addnclem3  37702  dvasin  37733  dvacos  37734  dvreasin  37735  dvreacos  37736  areacirclem1  37737  cnvepima  38360  glbconN  39400  glbconNOLD  39401  pmodl42N  39875  2polssN  39939  cdleme20j  40342  trlcocnv  40744  trlcone  40752  lclkrlem2c  41533  readvrec2  42379  sn-mul01  42443  selvvvval  42583  diophrw  42757  wopprc  43029  onuniintrab  43225  fsovcnvlem  44012  sineq0ALT  44936  founiiun0  45194  iccdifioo  45524  itgvol0  45977  fourierdlem33  46149  etransclem32  46275  simpcntrab  46879  cycl3grtrilem  47938  gpg3kgrtriexlem2  48066  gpgprismgr4cycllem3  48076  gsumdifsndf  48136  zlmodzxzadd  48313  cosn  48792  oppcendc  48973  resccatlem  49020  resccat  49021  0funcg2  49029  imaf1hom  49047