Theorem syl5eq 1562

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
syl5eq.1	⊢ (φ → A = B)
syl5eq.2	⊢ C = A

Assertion

Ref	Expression
syl5eq	⊢ (φ → C = B)

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.2	. . 3 ⊢ C = A
2	1	a1i 8	. 2 ⊢ (φ → C = A)
3		syl5eq.1	. 2 ⊢ (φ → A = B)
4	2, 3	eqtrd 1550	1 ⊢ (φ → C = B)

Syntax hints:   → wi 3   = wceq 992

This theorem is referenced by:  syl5req 1563  syl5eqr 1564  3eqtr4g 1574  csbconstgf 2061  csbvarg 2072  csbiegft 2081  csbabg 2095  ssin 2284  uneqin 2308  prprc2 2516  difsnid 2531  opprc1 2563  sucprc 3048  orduniss2 3187  relop 3365  resabs1 3478  resabs2 3479  resopab2 3488  imasng 3516  ndmima 3526  xpdisj1 3553  xpdisj2 3554  resdisj 3556  rnxp 3557  unixp 3622  fnun 3700  fnresdisj 3703  f1orescnv 3812  resdif 3816  fvprc 3832  fnrnfv 3870  fvopab4gf 3892  fvopabn 3897  fvopabgf 3898  fvopabnf 3899  fvopab6 3905  fvsnun2 3908  elrnopabg 3914  fopab2 3937  rnssopab 3939  fopabco 3946  funiunfv 3980  oprprc1 4042  fnoprabg 4072  oprabval2gf 4086  oprabval6g 4093  oprvconst2 4101  ndmoprg 4104  caoprmo 4131  1stval 4142  2ndval 4143  curry1 4193  curry2 4196  tz7.44-3 4231  rdgsucopab 4247  rdgsucopabn 4248  rdglim2 4250  fr0g 4253  frsucopab 4255  oa1suc 4300  om1 4312  oe1 4314  oarec 4332  oaabs 4392  map0b 4484  fodomr 4628  mapenlem1 4636  mapenlem2 4637  xpmapenlem5 4647  phplem2 4656  unifi 4701  fodomfi 4709  suppr 4733  supsn 4734  supsnALT 4735  tz9.12lem3 4807  rankonid 4841  rankxplim2 4859  ac6lem 4900  kmlem11 4921  zorn2 4942  oncardval 4965  cardval 4973  unxpdomlem 4993  nnacda 5090  1qec 5222  recrecpq 5227  ltaddpq 5233  ltexpq 5234  halfpq 5236  addclprlem1 5272  addclprlem2 5273  mulclprlem 5275  1idpr 5287  prlem934a 5291  prlem934b 5292  ltexprlem7 5302  ltaprlem 5304  prlem936a 5307  mulcmpblnrlem 5336  0idsr 5360  1idsr 5361  recexsrlem 5366  sqgt0sr 5369  ssgt0sr 5371  mulresr 5411  ax0id 5435  ax1id 5436  axcnre 5440  csbnegg 5518  negid 5533  divcan4zi 5900  lbinfm 6216  dfinfmr 6235  infmsup 6236  supxr 6249  supxrmnf 6255  uzindOLD 6379  quoremz 6451  quoremnn0 6453  intfracq 6455  ioojoin 6543  uzrdginii 6667  uzrdginip1i 6669  seq1suclem 6681  limsupval 6724  seq0valt 6731  seqzfval 6732  seq1seq01 6739  seq0p1 6746  seqzres2 6756  exp1 6768  expp1 6769  sqval 6806  discrlem2 6858  discrlem3 6859  sqrsqi 6921  crulem 6937  imre 6974  abs00i 7044  absidi 7063  cjdivi 7091  abs1mi 7107  faclbnd 7148  faclbnd2 7149  sumeqfv 7200  dffsum 7201  fsumserzfi 7203  serzfsum 7207  fsum1fi 7210  fsumadd 7225  csbfsum 7230  fsumshft 7234  binomlem1 7269  binomlem2 7270  binomlem4 7272  iserzexi 7349  dfisum 7395  isumvaltfi 7397  isumval2 7398  isum1clim 7401  isumcmpii 7419  geoisum 7447  geoisum1 7449  fsum0diag2 7464  divccncf 7485  eftlex 7583  ef1tlubi 7587  ef01tlubi 7591  absef01tlubi 7593  ef4p 7608  resinval 7641  recosval 7642  absefib 7693  efieq1re 7694  acdc3lem 7697  acdclem 7706  ruclem18 7739  ruclem19 7740  ruclem20 7741  ruclem21 7742  cnconst 7990  metssba 8019  metreslem 8032  metres 8033  blin 8062  opnfval 8067  methaus 8093  cncfmet 8116  remetdval 8119  bcthlem15 8224  bcth 8243  grpinvfval 8283  grpdivfval 8299  gxoprval 8313  resgrprn 8336  issubgi 8364  ghgrpilem1 8374  vcnegneg 8440  vafval 8469  bafval 8470  smfval 8471  0vfval 8472  vsfval 8501  nvnncan 8530  nvm1 8539  nvpi 8541  nvmtri 8546  imsval 8563  vacnlem5 8586  vacnlem6 8587  vacn 8588  nmcn 8593  ipfval 8606  ipval2 8611  ipcj 8621  ip1cnilem5 8631  sspval 8636  lnoval 8667  nmofval 8679  bloval 8696  0ofval 8702  nmlno0 8710  nmlnoubi 8711  ajfval 8724  hmoval 8725  ipdir 8758  ipass 8761  pythi 8766  ajfun 8777  minveclem19 8823  psref 8911  psrn 8912  spwval 8921  spwnex 8923  pilem3 8940  sinperlem1 8953  sin2pim 8959  cos2pim 8960  sinmpi 8961  cosmpi 8962  sinppi 8963  cosppi 8964  sinhalfpip 8966  sinhalfpim 8967  coshalfpip 8968  coshalfpim 8969  sineq0re 8985  shftefif1olem 9013  eflog 9032  logef 9034  hv2times 9203  bcseqi 9262  normpythi 9285  hhssnvt 9411  hhsssh 9415  pjthlem7 9501  pjoc1i 9540  chsupid 9587  h1de2i 9752  spanunsni 9778  cmcmlem 9810  cmbr3i 9819  fh1 9837  fh2 9838  hoival 9961  hoico1 9962  hoico2 9963  ho2times 10025  eigposi 10042  nmcopexlem2 10231  lnfnmuli 10252  nmcfnexlem2 10260  cnlnadjlem4 10282  cnlnadjlem5 10283  kbass5 10333  pjnmopi 10355  pjclem3 10406  pjadj2coi 10413  sto1i 10444  strlem3a 10460  strlem4 10462  hstrlem3a 10468  hstrlem4 10470  dmdbr5 10516  mdexchi 10543  superpos 10562  atomli 10591  atcvatlem 10594  irredlem2 10600  irredlem3 10601  atabsi 10610  mdsymlem1 10612  dmdbr6ati 10632  symgoprv 10689  cayleylem2 10695  cayleythlem 10698  fvopab2a 10747  imfstnrelc 10810  dupos1 10876  idrval 10904  on1el3 10962  rngunval2 10965  sallnei 11016  homcard 11045  trran 11159  domval 11177  codval 11178  idval 11179  cmpval 11180  ishomd 11245  idsubfun 11312  ordtypelem7 11433  omsubsuc 11438  cldbnd 11462  clsun 11465  subsubtop 11479  subcld 11480  compsub 11488  uncomp 11490  connsub 11502  subtopmetlem 11505  isnrm2 11613  fgf 11632  extbas2 11642  fixufil 11661  cnpfillim 11686  sfcls 11716  fcluscomplem 11732  dirref 11752  dirge 11754  tailf 11756  filnetlem5 11767  isga2 11774  gaid 11776  ssga 11777  gapm 11784  resoprab2 11809  cocnv 11815  subspabs 11903  blssp 11908  mettrifi2 11913  piececn 11955  txtop 11974  txuni 11975  tx1cn 11976  tx2cn 11977  uptx 11978  txcnoprab 11981  2txcn 11982  txopn 11984  ismtyres 12010  heiborlem9 12019  heiborlem11 12021  heiborlem18 12028  heiborlem35 12045  icccmp 12083  phtpyid 12091  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain