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

Theorem syl5reqr 2868
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 2827 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2866 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  resdmdfsn  5894  f0dom0  6556  f1o00  6642  fmpt  6866  fmptsn  6921  fninfp  6928  uniordint  7510  frnsuppeq  7831  mapsnd  8438  sbthlem4  8618  sbthlem6  8620  findcard2s  8747  elfiun  8882  cnfcom2  9153  rankxplim3  9298  rankxpsuc  9299  pm54.43  9417  axdc3lem4  9863  gruun  10216  recmulnq  10374  reclem3pr  10459  xrmineq  12561  xadddi2  12678  iooval2  12759  hashsng  13718  hashfun  13786  hashbc  13799  swrds2m  14291  isumclim3  15102  isummulc2  15105  iprodclim3  15342  bpolydiflem  15396  bpoly4  15401  fprodefsum  15436  ruclem4  15575  bitsshft  15812  phimullem  16104  pythagtriplem1  16141  1arithlem4  16250  fsets  16504  topnid  16697  pgrpsubgsymg  18466  odhash  18628  gsumzf1o  18961  gsumdifsnd  19010  pgpfaclem1  19132  fincygsubgodd  19163  subdrgint  19511  mplcoe1  20174  mplcoe5  20177  evlslem4  20216  ordtrest2  21740  ufildr  22467  tsmsres  22679  zlmclm  23643  cphipval2  23771  csschl  23906  rrxcph  23922  volinun  24074  uniioombllem4  24114  itg1climres  24242  limcco  24418  vieta1lem2  24827  coseq00topi  25015  tangtx  25018  coskpi  25035  advlog  25164  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  dvcncxp1  25251  loglesqrt  25266  ang180lem3  25316  dquart  25358  atans2  25436  basellem8  25592  chtub  25715  bposlem6  25792  lgsquadlem2  25884  logdivsum  26036  log2sumbnd  26047  spthispth  27434  ipval3  28413  siii  28557  cm2j  29324  pjssmii  29385  opsqrlem1  29844  hmopidmchi  29855  hmopidmpji  29856  pjcmul1i  29905  mddmd2  30013  cvexchlem  30072  dmdbr6ati  30127  difeq  30207  difuncomp  30232  ffsrn  30391  symgcom2  30655  cycpmcl  30685  cycpm2tr  30688  qusdimsum  30923  ordtprsuni  31061  ordtrest2NEW  31065  zzsnm  31101  measun  31369  sxbrsigalem2  31443  carsgsigalem  31472  eulerpartlemgu  31534  gsumnunsn  31710  signsplypnf  31719  logdivsqrle  31820  cvmlift2lem12  32458  satf0suc  32520  nepss  32845  nodenselem5  33089  fwddifnp1  33523  finxpreclem1  34552  finxpreclem3  34556  poimirlem31  34804  ismblfin  34814  dvtan  34823  itg2addnclem3  34826  dvasin  34859  dvacos  34860  dvreasin  34861  dvreacos  34862  areacirclem1  34863  cnvepima  35475  glbconN  36393  pmodl42N  36867  2polssN  36931  cdleme20j  37334  trlcocnv  37736  trlcone  37744  lclkrlem2c  38525  diophrw  39234  wopprc  39505  fsovcnvlem  40237  sineq0ALT  41148  founiiun0  41327  iccdifioo  41667  itgvol0  42129  fourierdlem33  42302  etransclem32  42428  simpcntrab  43004  gsumdifsndf  43965  submefmnd  43992  zlmodzxzadd  44334
  Copyright terms: Public domain W3C validator