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

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

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2834 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2874 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2818
This theorem is referenced by:  resdmdfsn  5682  f0dom0  6326  f1o00  6412  fmpt  6629  fmptsn  6685  fninfp  6692  uniordint  7267  frnsuppeq  7571  mapsnd  8164  sbthlem4  8342  sbthlem6  8344  findcard2s  8470  elfiun  8605  cnfcom2  8876  rankxplim3  9021  rankxpsuc  9022  pm54.43  9139  axdc3lem4  9590  gruun  9943  recmulnq  10101  reclem3pr  10186  xrmineq  12299  xadddi2  12415  iooval2  12496  hashsng  13449  hashfun  13513  hashbc  13526  swrds2m  14062  isumclim3  14865  isummulc2  14868  iprodclim3  15103  bpolydiflem  15157  bpoly4  15162  fprodefsum  15197  ruclem4  15337  bitsshft  15570  phimullem  15855  pythagtriplem1  15892  1arithlem4  16001  fsets  16255  topnid  16449  pgrpsubgsymg  18178  odhash  18340  gsumzf1o  18666  gsumdifsnd  18713  pgpfaclem1  18834  mplcoe1  19826  mplcoe5  19829  evlslem4  19868  ordtrest2  21379  ufildr  22105  tsmsres  22317  zlmclm  23281  cphipval2  23409  csschl  23544  rrxcph  23560  volinun  23712  uniioombllem4  23752  itg1climres  23880  limcco  24056  vieta1lem2  24465  coseq00topi  24654  tangtx  24657  coskpi  24672  advlog  24799  advlogexp  24800  logtayl  24805  logccv  24808  dvcxp1  24883  dvcncxp1  24886  loglesqrt  24901  ang180lem3  24951  dquart  24993  atans2  25071  basellem8  25227  chtub  25350  bposlem6  25427  lgsquadlem2  25519  logdivsum  25635  log2sumbnd  25646  spthispth  27028  ipval3  28119  siii  28263  cm2j  29034  pjssmii  29095  opsqrlem1  29554  hmopidmchi  29565  hmopidmpji  29566  pjcmul1i  29615  mddmd2  29723  cvexchlem  29782  dmdbr6ati  29837  difeq  29903  difuncomp  29917  ffsrn  30052  ordtprsuni  30510  ordtrest2NEW  30514  zzsnm  30550  measun  30819  sxbrsigalem2  30893  carsgsigalem  30922  eulerpartlemgu  30984  gsumnunsn  31161  signsplypnf  31174  logdivsqrle  31277  cvmlift2lem12  31842  nepss  32143  nodenselem5  32377  fwddifnp1  32811  finxpreclem1  33771  finxpreclem3  33775  poimirlem31  33984  ismblfin  33994  dvtan  34003  itg2addnclem3  34006  dvasin  34039  dvacos  34040  dvreasin  34041  dvreacos  34042  areacirclem1  34043  glbconN  35452  pmodl42N  35926  2polssN  35990  cdleme20j  36393  trlcocnv  36795  trlcone  36803  lclkrlem2c  37584  diophrw  38166  wopprc  38440  fsovcnvlem  39147  sineq0ALT  39991  iccdifioo  40537  itgvol0  40978  fourierdlem33  41151  etransclem32  41277  zlmodzxzadd  42983  gsumdifsndf  42991
  Copyright terms: Public domain W3C validator