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 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  resdmdfsn  5990  f0dom0  6718  f1o00  6809  fmpt  7055  fmptsn  7113  fninfp  7120  uniordint  7746  fsuppeq  8117  fsuppeqg  8118  mapsnd  8824  sbthlem4  9018  sbthlem6  9020  findcard2s  9090  ssfi  9097  elfiun  9333  cnfcom2  9611  rankxplim3  9793  rankxpsuc  9794  pm54.43  9913  axdc3lem4  10363  gruun  10717  recmulnq  10875  reclem3pr  10960  xrmineq  13095  xadddi2  13212  iooval2  13294  hashsng  14292  hashfun  14360  hashbc  14376  swrds2m  14864  isumclim3  15682  isummulc2  15685  iprodclim3  15923  bpolydiflem  15977  bpoly4  15982  fprodefsum  16018  ruclem4  16159  bitsshft  16402  phimullem  16706  pythagtriplem1  16744  1arithlem4  16854  fsets  17096  topnid  17355  submefmnd  18820  pgrpsubgsymg  19338  odhash  19503  gsumzf1o  19841  gsumdifsnd  19890  pgpfaclem1  20012  fincygsubgodd  20043  subdrgint  20736  mplcoe1  21992  mplcoe5  21995  evlslem4  22031  ordtrest2  23148  ufildr  23875  tsmsres  24088  zlmclm  25068  cphipval2  25197  csschl  25332  rrxcph  25348  volinun  25503  uniioombllem4  25543  itg1climres  25671  limcco  25850  vieta1lem2  26275  coseq00topi  26467  tangtx  26470  coskpi  26488  advlog  26619  advlogexp  26620  logtayl  26625  logccv  26628  dvcxp1  26705  dvcncxp1  26708  loglesqrt  26727  ang180lem3  26777  dquart  26819  atans2  26897  basellem8  27054  chtub  27179  bposlem6  27256  lgsquadlem2  27348  logdivsum  27500  log2sumbnd  27511  nodenselem5  27656  oldsuc  27882  precsexlem3  28205  spthispth  29797  ipval3  30784  siii  30928  cm2j  31695  pjssmii  31756  opsqrlem1  32215  hmopidmchi  32226  hmopidmpji  32227  pjcmul1i  32276  mddmd2  32384  cvexchlem  32443  dmdbr6ati  32498  difeq  32593  difuncomp  32628  ffsrn  32807  fzo0opth  32883  symgcom2  33166  cycpmcl  33198  cycpm2tr  33201  rhmimaidl  33513  drngidlhash  33515  1arithidomlem2  33617  qusdimsum  33785  2sqr3minply  33937  cos9thpiminplylem2  33940  zarcmplem  34038  ordtprsuni  34076  ordtrest2NEW  34080  zzsnm  34116  measun  34368  sxbrsigalem2  34443  carsgsigalem  34472  eulerpartlemgu  34534  gsumnunsn  34698  signsplypnf  34707  logdivsqrle  34807  cvmlift2lem12  35508  satf0suc  35570  nepss  35912  fwddifnp1  36359  finxpreclem1  37594  finxpreclem3  37598  poimirlem31  37852  ismblfin  37862  dvtan  37871  itg2addnclem3  37874  dvasin  37905  dvacos  37906  dvreasin  37907  dvreacos  37908  areacirclem1  37909  cnvepima  38530  glbconN  39637  pmodl42N  40111  2polssN  40175  cdleme20j  40578  trlcocnv  40980  trlcone  40988  lclkrlem2c  41769  readvrec2  42616  sn-00idlem3  42655  sn-mul01  42681  selvvvval  42828  diophrw  43001  wopprc  43272  onuniintrab  43468  fsovcnvlem  44254  sineq0ALT  45177  founiiun0  45434  iccdifioo  45761  itgvol0  46212  fourierdlem33  46384  etransclem32  46510  simpcntrab  47114  chnsubseqwl  47123  cycl3grtrilem  48192  gpg3kgrtriexlem2  48330  gpgprismgr4cycllem3  48343  gsumdifsndf  48427  zlmodzxzadd  48604  cosn  49079  oppcendc  49263  resccatlem  49318  resccat  49319  0funcg2  49329  imaf1hom  49353