Theorem syl5eq 2182

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 2170	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  syl5req  2183  syl5eqr  2184  3eqtr3a  2194  3eqtr4g  2195  csbtt  3009  csbvarg  3025  csbie2g  3045  rabbi2dva  3279  csbprc  3403  disjssun  3421  disjpr2  3582  prprc2  3627  difprsn2  3655  opprc  3721  intsng  3800  riinm  3880  iinxsng  3881  iunxprg  3888  rintm  3900  sucprc  4329  unisucg  4331  xpriindim  4672  relop  4684  dmxpm  4754  riinint  4795  resabs1  4843  resabs2  4845  resima2  4848  xpssres  4849  resopab2  4861  imasng  4899  ndmima  4911  xpdisj1  4958  xpdisj2  4959  djudisj  4961  resdisj  4962  rnxpm  4963  xpima1  4980  xpima2m  4981  dmsnsnsng  5011  rnsnopg  5012  rnpropg  5013  mptiniseg  5028  dfco2a  5034  relcoi1  5065  unixpm  5069  iotaval  5094  funtp  5171  fnun  5224  fnresdisj  5228  fnima  5236  fnimaeq0  5239  fcoi1  5298  f1orescnv  5376  foun  5379  resdif  5382  tz6.12-2  5405  fveu  5406  tz6.12-1  5441  fvun2  5481  fvopab3ig  5488  f1oresrab  5578  dfmptg  5592  ressnop0  5594  fvunsng  5607  fnsnsplitss  5612  fsnunfv  5614  fvpr1  5617  fvpr2  5618  fvpr1g  5619  fvpr2g  5620  fvtp1g  5621  fvtp2g  5622  fvtp3g  5623  fvtp2  5625  fvtp3  5626  f1oiso2  5721  riotaund  5757  ovprc  5799  resoprab2  5861  fnoprabg  5865  ovidig  5881  ovigg  5884  ov6g  5901  ovconst2  5915  offval2  5990  ot1stg  6043  ot2ndg  6044  ot3rdgg  6045  fmpoco  6106  algrflemg  6120  tpostpos2  6155  rdgisuc1  6274  frec0g  6287  frecsuclem  6296  frecrdg  6298  oasuc  6353  oa1suc  6356  omsuc  6361  nnm1  6413  nnm2  6414  dfec2  6425  errn  6444  ixpsnval  6588  ixpintm  6612  mapen  6733  xpmapenlem  6736  phplem2  6740  undifdc  6805  fisseneq  6813  ssfirab  6815  eqinfti  6900  infvalti  6902  infsnti  6910  casef  6966  caseinl  6969  caseinr  6970  djudom  6971  ctssdccl  6989  exmidfodomrlemim  7050  1qec  7189  mulidnq  7190  addpinq1  7265  suplocexprlem2b  7515  suplocexprlemlub  7525  0idsr  7568  1idsr  7569  caucvgsrlemoffres  7601  caucvgsr  7603  mulresr  7639  pitonnlem2  7648  ax1rid  7678  axcnre  7682  negid  8002  subneg  8004  negneg  8005  dfinfre  8707  2times  8841  infrenegsupex  9382  rexneg  9606  xaddpnf2  9623  xaddmnf1  9624  xaddmnf2  9625  fseq1p1m1  9867  fzosplitprm1  10004  intfracq  10086  frec2uz0d  10165  frec2uzrdg  10175  frecuzrdg0  10179  frecuzrdgg  10182  frecuzrdg0t  10188  seq3val  10224  seqvalcd  10225  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsum  10266  sqval  10344  iexpcyc  10390  binom3  10402  faclbnd  10480  faclbnd2  10481  bcn1  10497  hashinfom  10517  hashennn  10519  hashxp  10565  shftlem  10581  shftuz  10582  shftidt  10598  reim0  10626  remullem  10636  resqrexlemf1  10773  resqrexlemcalc3  10781  absexpzap  10845  absimle  10849  amgm2  10883  minmax  10994  xrmaxiflemval  11012  xrmaxadd  11023  infxrnegsupex  11025  xrminmax  11027  summodc  11145  fsum3  11149  sumsnf  11171  sumsns  11177  isumclim3  11185  isumge0  11192  fsump1i  11195  fsum2dlemstep  11196  fisumcom2  11200  fsumshftm  11207  fsumconst  11216  fsumiun  11239  hashrabrex  11243  hashuni  11244  binom11  11248  isumsplit  11253  geo2sum  11276  mertensabs  11299  efgt1p2  11390  efgt1p  11391  resinval  11411  recosval  11412  cosadd  11433  ef01bndlem  11452  eirraplem  11472  ialgr0  11714  algrp1  11716  eucalg  11729  phiprmpw  11887  phiprm  11888  ennnfonelem0  11907  ennnfonelemfun  11919  ennnfonelemf1  11920  ennnfonelemrn  11921  ctinfomlemom  11929  ndxid  11972  setsfun0  11984  setsresg  11986  setscom  11988  strslfv2d  11990  ressid2  12007  ressval2  12008  tgidm  12232  tgrest  12327  ssidcn  12368  txcnmpt  12431  txcn  12433  blres  12592  mopnval  12600  remetdval  12697  divccncfap  12735  cncfmet  12737  cncfcncntop  12738  cnplimcim  12794  cnplimclemr  12796  limccnpcntop  12802  limccnp2cntop  12804  dvexp  12833  sin0pilem1  12851  pilem3  12853  ef2kpi  12876  sin2pim  12883  cos2pim  12884  sinmpi  12885  cosmpi  12886  sinppi  12887  cosppi  12888  sinhalfpip  12890  sinhalfpim  12891  coshalfpip  12892  coshalfpim  12893  tangtx  12908  ex-ceil  12927  qdencn  13211  cvgcmp2nlemabs  13216  trilpolemlt1  13223