Theorem syl5eq 2144

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eq.1	⊢ 𝐴 = 𝐵
syl5eq.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl5eq.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrd 2132	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  syl5req  2145  syl5eqr  2146  3eqtr3a  2156  3eqtr4g  2157  csbtt  2965  csbvarg  2980  csbie2g  3000  rabbi2dva  3231  csbprc  3355  disjssun  3373  disjpr2  3534  prprc2  3579  difprsn2  3607  opprc  3673  intsng  3752  riinm  3832  iinxsng  3833  rintm  3851  sucprc  4272  unisucg  4274  xpriindim  4615  relop  4627  dmxpm  4697  riinint  4736  resabs1  4784  resabs2  4786  resima2  4789  xpssres  4790  resopab2  4802  imasng  4840  ndmima  4852  xpdisj1  4899  xpdisj2  4900  djudisj  4902  resdisj  4903  rnxpm  4904  xpima1  4921  xpima2m  4922  dmsnsnsng  4952  rnsnopg  4953  rnpropg  4954  mptiniseg  4969  dfco2a  4975  relcoi1  5006  unixpm  5010  iotaval  5035  funtp  5112  fnun  5165  fnresdisj  5169  fnima  5177  fnimaeq0  5180  fcoi1  5239  f1orescnv  5317  foun  5320  resdif  5323  tz6.12-2  5344  fveu  5345  tz6.12-1  5380  fvun2  5420  fvopab3ig  5427  f1oresrab  5517  dfmptg  5531  ressnop0  5533  fvunsng  5546  fnsnsplitss  5551  fsnunfv  5553  fvpr1  5556  fvpr2  5557  fvpr1g  5558  fvpr2g  5559  fvtp1g  5560  fvtp2g  5561  fvtp3g  5562  fvtp2  5564  fvtp3  5565  f1oiso2  5660  riotaund  5696  ovprc  5738  resoprab2  5800  fnoprabg  5804  ovidig  5820  ovigg  5823  ov6g  5840  ovconst2  5854  offval2  5928  ot1stg  5981  ot2ndg  5982  ot3rdgg  5983  fmpoco  6043  algrflemg  6057  tpostpos2  6092  rdgisuc1  6211  frec0g  6224  frecsuclem  6233  frecrdg  6235  oasuc  6290  oa1suc  6293  omsuc  6298  nnm1  6350  nnm2  6351  dfec2  6362  errn  6381  ixpsnval  6525  ixpintm  6549  mapen  6669  xpmapenlem  6672  phplem2  6676  undifdc  6741  fisseneq  6749  ssfirab  6750  eqinfti  6822  infvalti  6824  infsnti  6832  casef  6888  caseinl  6891  caseinr  6892  djudom  6893  exmidfodomrlemim  6966  1qec  7097  mulidnq  7098  addpinq1  7173  0idsr  7463  1idsr  7464  caucvgsrlemoffres  7495  caucvgsr  7497  mulresr  7525  pitonnlem2  7534  ax1rid  7562  axcnre  7566  negid  7880  subneg  7882  negneg  7883  dfinfre  8572  2times  8700  infrenegsupex  9239  rexneg  9454  xaddpnf2  9471  xaddmnf1  9472  xaddmnf2  9473  fseq1p1m1  9715  fzosplitprm1  9852  intfracq  9934  frec2uz0d  10013  frec2uzrdg  10023  frecuzrdg0  10027  frecuzrdgg  10030  frecuzrdg0t  10036  seq3val  10072  seqvalcd  10073  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsum  10114  sqval  10192  iexpcyc  10238  binom3  10250  faclbnd  10328  faclbnd2  10329  bcn1  10345  hashinfom  10365  hashennn  10367  hashxp  10413  shftlem  10429  shftuz  10430  shftidt  10446  reim0  10474  remullem  10484  resqrexlemf1  10620  resqrexlemcalc3  10628  absexpzap  10692  absimle  10696  amgm2  10730  minmax  10840  xrmaxiflemval  10858  xrmaxadd  10869  infxrnegsupex  10871  xrminmax  10873  summodc  10991  fsum3  10995  sumsnf  11017  sumsns  11023  isumclim3  11031  isumge0  11038  fsump1i  11041  fsum2dlemstep  11042  fisumcom2  11046  fsumshftm  11053  fsumconst  11062  fsumiun  11085  hashrabrex  11089  hashuni  11090  binom11  11094  isumsplit  11099  geo2sum  11122  mertensabs  11145  efgt1p2  11199  efgt1p  11200  resinval  11220  recosval  11221  cosadd  11242  ef01bndlem  11261  eirraplem  11278  ialgr0  11518  algrp1  11520  eucalg  11533  phiprmpw  11690  phiprm  11691  ennnfonelem0  11710  ennnfonelemfun  11722  ennnfonelemf1  11723  ennnfonelemrn  11724  ctinfomlemom  11732  ndxid  11765  setsfun0  11777  setsresg  11779  setscom  11781  strslfv2d  11783  ressid2  11800  ressval2  11801  tgidm  12025  tgrest  12120  ssidcn  12160  txcnmpt  12223  txcn  12225  blres  12362  mopnval  12370  remetdval  12458  divccncfap  12490  cncfmet  12492  cncfcncntop  12493  cnplimcim  12516  limccnpcntop  12520  ex-ceil  12541  qdencn  12806  cvgcmp2nlemabs  12811  trilpolemlt1  12818