Theorem syl5reqr 2848

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

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2807	. 2 ⊢ 𝐴 = 𝐵
3		syl5reqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5req 2846	1 ⊢ (𝜑 → 𝐶 = 𝐴)

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:  resdmdfsn  5868  f0dom0  6537  f1o00  6624  fmpt  6851  fmptsn  6906  fninfp  6913  uniordint  7501  frnsuppeq  7825  mapsnd  8433  sbthlem4  8614  sbthlem6  8616  findcard2s  8743  elfiun  8878  cnfcom2  9149  rankxplim3  9294  rankxpsuc  9295  pm54.43  9414  axdc3lem4  9864  gruun  10217  recmulnq  10375  reclem3pr  10460  xrmineq  12561  xadddi2  12678  iooval2  12759  hashsng  13726  hashfun  13794  hashbc  13807  swrds2m  14294  isumclim3  15106  isummulc2  15109  iprodclim3  15346  bpolydiflem  15400  bpoly4  15405  fprodefsum  15440  ruclem4  15579  bitsshft  15814  phimullem  16106  pythagtriplem1  16143  1arithlem4  16252  fsets  16508  topnid  16701  submefmnd  18052  pgrpsubgsymg  18529  odhash  18691  gsumzf1o  19025  gsumdifsnd  19074  pgpfaclem1  19196  fincygsubgodd  19227  subdrgint  19575  mplcoe1  20705  mplcoe5  20708  evlslem4  20747  ordtrest2  21809  ufildr  22536  tsmsres  22749  zlmclm  23717  cphipval2  23845  csschl  23980  rrxcph  23996  volinun  24150  uniioombllem4  24190  itg1climres  24318  limcco  24496  vieta1lem2  24907  coseq00topi  25095  tangtx  25098  coskpi  25115  advlog  25245  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  dvcncxp1  25332  loglesqrt  25347  ang180lem3  25397  dquart  25439  atans2  25517  basellem8  25673  chtub  25796  bposlem6  25873  lgsquadlem2  25965  logdivsum  26117  log2sumbnd  26128  spthispth  27515  ipval3  28492  siii  28636  cm2j  29403  pjssmii  29464  opsqrlem1  29923  hmopidmchi  29934  hmopidmpji  29935  pjcmul1i  29984  mddmd2  30092  cvexchlem  30151  dmdbr6ati  30206  difeq  30289  difuncomp  30317  ffsrn  30491  symgcom2  30778  cycpmcl  30808  cycpm2tr  30811  rhmimaidl  31017  qusdimsum  31112  zarcmplem  31234  ordtprsuni  31272  ordtrest2NEW  31276  zzsnm  31312  measun  31580  sxbrsigalem2  31654  carsgsigalem  31683  eulerpartlemgu  31745  gsumnunsn  31921  signsplypnf  31930  logdivsqrle  32031  cvmlift2lem12  32674  satf0suc  32736  nepss  33061  nodenselem5  33305  fwddifnp1  33739  finxpreclem1  34806  finxpreclem3  34810  poimirlem31  35088  ismblfin  35098  dvtan  35107  itg2addnclem3  35110  dvasin  35141  dvacos  35142  dvreasin  35143  dvreacos  35144  areacirclem1  35145  cnvepima  35754  glbconN  36673  pmodl42N  37147  2polssN  37211  cdleme20j  37614  trlcocnv  38016  trlcone  38024  lclkrlem2c  38805  sn-mul01  39562  diophrw  39700  wopprc  39971  fsovcnvlem  40714  sineq0ALT  41643  founiiun0  41817  iccdifioo  42152  itgvol0  42610  fourierdlem33  42782  etransclem32  42908  simpcntrab  43484  gsumdifsndf  44441  zlmodzxzadd  44760