Theorem syl5reqr 2871

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 2830	. 2 ⊢ 𝐴 = 𝐵
3		syl5reqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5req 2869	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  resdmdfsn  5895  f0dom0  6557  f1o00  6643  fmpt  6868  fmptsn  6923  fninfp  6930  uniordint  7515  frnsuppeq  7836  mapsnd  8444  sbthlem4  8624  sbthlem6  8626  findcard2s  8753  elfiun  8888  cnfcom2  9159  rankxplim3  9304  rankxpsuc  9305  pm54.43  9423  axdc3lem4  9869  gruun  10222  recmulnq  10380  reclem3pr  10465  xrmineq  12567  xadddi2  12684  iooval2  12765  hashsng  13724  hashfun  13792  hashbc  13805  swrds2m  14297  isumclim3  15108  isummulc2  15111  iprodclim3  15348  bpolydiflem  15402  bpoly4  15407  fprodefsum  15442  ruclem4  15581  bitsshft  15818  phimullem  16110  pythagtriplem1  16147  1arithlem4  16256  fsets  16510  topnid  16703  submefmnd  18054  pgrpsubgsymg  18531  odhash  18693  gsumzf1o  19026  gsumdifsnd  19075  pgpfaclem1  19197  fincygsubgodd  19228  subdrgint  19576  mplcoe1  20240  mplcoe5  20243  evlslem4  20282  ordtrest2  21806  ufildr  22533  tsmsres  22746  zlmclm  23710  cphipval2  23838  csschl  23973  rrxcph  23989  volinun  24141  uniioombllem4  24181  itg1climres  24309  limcco  24485  vieta1lem2  24894  coseq00topi  25082  tangtx  25085  coskpi  25102  advlog  25231  advlogexp  25232  logtayl  25237  logccv  25240  dvcxp1  25315  dvcncxp1  25318  loglesqrt  25333  ang180lem3  25383  dquart  25425  atans2  25503  basellem8  25659  chtub  25782  bposlem6  25859  lgsquadlem2  25951  logdivsum  26103  log2sumbnd  26114  spthispth  27501  ipval3  28480  siii  28624  cm2j  29391  pjssmii  29452  opsqrlem1  29911  hmopidmchi  29922  hmopidmpji  29923  pjcmul1i  29972  mddmd2  30080  cvexchlem  30139  dmdbr6ati  30194  difeq  30274  difuncomp  30299  ffsrn  30459  symgcom2  30723  cycpmcl  30753  cycpm2tr  30756  qusdimsum  31019  ordtprsuni  31157  ordtrest2NEW  31161  zzsnm  31197  measun  31465  sxbrsigalem2  31539  carsgsigalem  31568  eulerpartlemgu  31630  gsumnunsn  31806  signsplypnf  31815  logdivsqrle  31916  cvmlift2lem12  32556  satf0suc  32618  nepss  32943  nodenselem5  33187  fwddifnp1  33621  finxpreclem1  34664  finxpreclem3  34668  poimirlem31  34917  ismblfin  34927  dvtan  34936  itg2addnclem3  34939  dvasin  34972  dvacos  34973  dvreasin  34974  dvreacos  34975  areacirclem1  34976  cnvepima  35588  glbconN  36507  pmodl42N  36981  2polssN  37045  cdleme20j  37448  trlcocnv  37850  trlcone  37858  lclkrlem2c  38639  diophrw  39349  wopprc  39620  fsovcnvlem  40352  sineq0ALT  41264  founiiun0  41444  iccdifioo  41784  itgvol0  42246  fourierdlem33  42419  etransclem32  42545  simpcntrab  43121  gsumdifsndf  44082  zlmodzxzadd  44400