MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5req Structured version   Visualization version   GIF version

Theorem syl5req 2812
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1 𝐴 = 𝐵
syl5req.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5req (𝜑𝐶 = 𝐴)

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3 𝐴 = 𝐵
2 syl5req.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2syl5eq 2811 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2771 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758
This theorem is referenced by:  syl5reqr  2814  opeqsng  5122  opeqsnOLD  5124  relop  5441  ordintdif  5957  iotanul  6046  funopg  6102  funcnvres  6145  fpropnf1  6716  csbriota  6815  csbov123  6883  mpt2curryd  7598  nneob  7937  sucdom2  8363  unblem2  8420  pwfilem  8467  kmlem2  9226  kmlem11  9235  kmlem12  9236  cflim3  9337  1idsr  10172  recextlem1  10911  quoremz  12862  quoremnn0ALT  12864  intfrac2  12865  hashprg  13384  hashfacen  13439  leiso  13444  ccatrid  13558  swrdccat3aOLD  13748  repsw2  13981  repsw3  13982  cvgcmpce  14836  explecnv  14883  risefallfac  15039  ramub1lem1  16011  ressress  16213  subsubc  16780  grp1inv  17792  psgnunilem1  18178  psgn0fv0  18197  psgnsn  18206  efginvrel2  18406  efgredleme  18422  efgcpbllemb  18434  frgpnabllem1  18542  gsumzaddlem  18587  gsumzmhm  18603  fsfnn0gsumfsffz  18645  dprd2da  18708  dpjcntz  18718  dpjdisj  18719  dpjlsm  18720  dpjidcl  18724  ablfac1lem  18734  ablfac1eu  18739  lmhmlsp  19321  mplmon2mul  19774  frlmip  20393  1marepvmarrepid  20658  m1detdiag  20680  cramerimplem2  20769  pmatcollpw3lem  20867  chpscmatgsumbin  20928  chpscmatgsummon  20929  cayhamlem2  20968  neitr  21264  fixufil  22005  trust  22312  restmetu  22654  nmfval2  22674  nmval2  22675  rerest  22886  xrrest  22889  xrge0gsumle  22915  rrxip  23467  voliunlem3  23610  volsup  23614  itg1addlem5  23758  itg2monolem1  23808  itg2cnlem2  23820  itgmpt  23840  iblcnlem1  23845  itgcnlem  23847  itgioo  23873  limcres  23941  mdegfval  24113  dgrlem  24276  coeidlem  24284  mcubic  24865  binom4  24868  dquartlem2  24870  amgm  25008  lgamgulmlem2  25047  eflgam  25062  wilthlem2  25086  rpvmasum2  25492  pntlemo  25587  wlkres  26858  3wlkond  27407  3cycld  27414  frgrncvvdeqlem3  27539  extwwlkfablem1OLD  27580  vc2OLD  27814  nvge0  27919  nmoo0  28037  bcsiALT  28427  pjchi  28682  shjshseli  28743  spanpr  28830  pjinvari  29441  mdslmd1lem2  29576  iundifdifd  29763  iundifdif  29764  fmptco1f1o  29819  gtiso  29862  rngurd  30170  esumpr2  30511  omssubaddlem  30743  eulerpartlemt  30815  ofcccat  31003  topjoin  32735  tailfval  32742  tailf  32745  dvasin  33851  dvacos  33852  opidon2OLD  34007  cdleme4  36126  cdleme22e  36232  cdleme22eALTN  36233  cdleme42a  36359  cdleme42d  36361  cdlemk20  36762  dih1dimatlem0  37216  lcfrlem2  37431  elrfi  37867  fzsplit1nn0  37927  rabdiophlem2  37976  eldioph4b  37985  diophren  37987  pell1qrgaplem  38047  rngunsnply  38352  compneOLD  39249  fmuldfeq  40385  limciccioolb  40423  ditgeq3d  40749  stoweidlem44  40830  dirkertrigeq  40887  fourierdlem32  40925  fourierdlem33  40926  fourierdlem42  40935  fourierdlem62  40954  fourierdlem84  40976  fourierdlem85  40977  fourierdlem97  40989  fourierdlem98  40990  fourierdlem102  40994  fourierdlem104  40996  fourierdlem113  41005  fourierdlem114  41006  fourierswlem  41016  fouriersw  41017  sssalgen  41122  meadjun  41248  deccarry  41987  fsumsplitsndif  42009  funcrngcsetcALT  42600
  Copyright terms: Public domain W3C validator