Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr2di Structured version   Visualization version   GIF version

Theorem eqtr2di 2850
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr2di.1 (𝜑𝐴 = 𝐵)
eqtr2di.2 𝐵 = 𝐶
Assertion
Ref Expression
eqtr2di (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2di
StepHypRef Expression
1 eqtr2di.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2di.2 . . 3 𝐵 = 𝐶
31, 2eqtrdi 2849 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2804 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791 This theorem is referenced by:  eqtr4id  2852  csbin  4350  csbif  4483  csbuni  4833  csbima12  5918  somincom  5965  resresdm  6061  csbfv12  6698  opabiotafun  6729  fvmptrabfv  6786  fndifnfp  6925  elxp4  7622  elxp5  7623  fo1stres  7710  fo2ndres  7711  eloprabi  7756  fo2ndf  7813  seqomlem2  8088  oev2  8149  odi  8206  fundmen  8584  xpsnen  8602  xpassen  8612  ac6sfi  8764  infeq5  9102  alephsuc3  10009  rankcf  10206  ine0  11082  nn0n0n1ge2  11970  fzval2  12908  fseq1p1m1  12996  fzosplitprm1  13162  hashfun  13814  hashf1  13831  hashtpg  13859  cshword  14164  wrd2pr2op  14316  wrd3tpop  14321  relexpsucrd  14404  relexpsucld  14405  fsum2dlem  15137  fprod2dlem  15346  ef4p  15478  sin01bnd  15550  odd2np1  15702  bitsinvp1  15808  smumullem  15851  oppcmon  17020  issubc2  17118  curf1cl  17490  curfcl  17494  cnvtsr  17844  sylow1lem1  18736  sylow2a  18757  ablsimpgfindlem1  19243  coe1fzgsumdlem  20971  evl1gsumdlem  21021  pmatcollpw3lem  21429  pptbas  21654  2ndcctbss  22101  txcmplem1  22287  qtopeu  22362  alexsubALTlem3  22695  ustuqtop5  22892  psmetdmdm  22953  xmetdmdm  22983  pcopt  23668  pcorevlem  23672  voliunlem1  24195  i1fima2  24324  iblabs  24473  dveflem  24623  deg1val  24741  abssinper  25157  mulcxplem  25319  dvatan  25565  lgamgulmlem2  25659  lgamgulmlem5  25662  lgseisenlem1  26003  dchrisumlem1  26117  pntlemr  26230  krippenlem  26528  cusgredg  27258  cusgrsizeindb0  27283  numclwlk1lem1  28198  numclwwlk3lem2lem  28212  grporndm  28337  vafval  28430  smfval  28432  hvmul0  28851  cmcmlem  29418  cmbr3i  29427  nmbdfnlbi  29876  nmcfnlbi  29879  nmopcoadji  29928  pjin2i  30020  hst1h  30054  xaddeq0  30547  gsumhashmul  30790  cycpmconjslem1  30895  archirngz  30917  esumcst  31498  eulerpartlems  31794  dstfrvunirn  31908  sgnmul  31976  subfacp1lem5  32610  cvmliftlem10  32720  fnessref  33965  fnemeet2  33975  poimirlem4  35212  poimirlem19  35227  poimirlem20  35228  poimirlem23  35231  poimirlem24  35232  poimirlem25  35233  poimirlem28  35236  ovoliunnfl  35250  voliunnfl  35252  volsupnfl  35253  itg2addnclem  35259  itg2addnc  35262  iblabsnc  35272  iblmulc2nc  35273  sdclem2  35331  blbnd  35376  ismgmOLD  35439  ismndo2  35463  rnresequniqs  35900  tendo0co2  38235  dvhfvadd  38538  dvh4dimN  38894  mzpcompact2lem  39863  diophrw  39871  eldioph2  39874  pellexlem5  39945  pell1qr1  39983  rmxy0  40035  wessf1ornlem  41981  cncfuni  42696  cncfiooicclem1  42703  fourierdlem38  42955  fourierdlem60  42976  fourierdlem61  42977  fourierdlem79  42995  fourierdlem112  43028  fourierswlem  43040  fouriersw  43041  fvmptrab  44016  fvmptrabdm  44017  fmtnofac2  44254  nn0sumshdiglem1  45201
 Copyright terms: Public domain W3C validator