ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5eq GIF version

Theorem syl5eq 2162
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
StepHypRef Expression
1 syl5eq.1 . . 3 𝐴 = 𝐵
21a1i 9 . 2 (𝜑𝐴 = 𝐵)
3 syl5eq.2 . 2 (𝜑𝐵 = 𝐶)
42, 3eqtrd 2150 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  syl5req  2163  syl5eqr  2164  3eqtr3a  2174  3eqtr4g  2175  csbtt  2985  csbvarg  3000  csbie2g  3020  rabbi2dva  3254  csbprc  3378  disjssun  3396  disjpr2  3557  prprc2  3602  difprsn2  3630  opprc  3696  intsng  3775  riinm  3855  iinxsng  3856  iunxprg  3863  rintm  3875  sucprc  4304  unisucg  4306  xpriindim  4647  relop  4659  dmxpm  4729  riinint  4770  resabs1  4818  resabs2  4820  resima2  4823  xpssres  4824  resopab2  4836  imasng  4874  ndmima  4886  xpdisj1  4933  xpdisj2  4934  djudisj  4936  resdisj  4937  rnxpm  4938  xpima1  4955  xpima2m  4956  dmsnsnsng  4986  rnsnopg  4987  rnpropg  4988  mptiniseg  5003  dfco2a  5009  relcoi1  5040  unixpm  5044  iotaval  5069  funtp  5146  fnun  5199  fnresdisj  5203  fnima  5211  fnimaeq0  5214  fcoi1  5273  f1orescnv  5351  foun  5354  resdif  5357  tz6.12-2  5380  fveu  5381  tz6.12-1  5416  fvun2  5456  fvopab3ig  5463  f1oresrab  5553  dfmptg  5567  ressnop0  5569  fvunsng  5582  fnsnsplitss  5587  fsnunfv  5589  fvpr1  5592  fvpr2  5593  fvpr1g  5594  fvpr2g  5595  fvtp1g  5596  fvtp2g  5597  fvtp3g  5598  fvtp2  5600  fvtp3  5601  f1oiso2  5696  riotaund  5732  ovprc  5774  resoprab2  5836  fnoprabg  5840  ovidig  5856  ovigg  5859  ov6g  5876  ovconst2  5890  offval2  5965  ot1stg  6018  ot2ndg  6019  ot3rdgg  6020  fmpoco  6081  algrflemg  6095  tpostpos2  6130  rdgisuc1  6249  frec0g  6262  frecsuclem  6271  frecrdg  6273  oasuc  6328  oa1suc  6331  omsuc  6336  nnm1  6388  nnm2  6389  dfec2  6400  errn  6419  ixpsnval  6563  ixpintm  6587  mapen  6708  xpmapenlem  6711  phplem2  6715  undifdc  6780  fisseneq  6788  ssfirab  6790  eqinfti  6875  infvalti  6877  infsnti  6885  casef  6941  caseinl  6944  caseinr  6945  djudom  6946  ctssdccl  6964  exmidfodomrlemim  7025  1qec  7164  mulidnq  7165  addpinq1  7240  suplocexprlem2b  7490  suplocexprlemlub  7500  0idsr  7543  1idsr  7544  caucvgsrlemoffres  7576  caucvgsr  7578  mulresr  7614  pitonnlem2  7623  ax1rid  7653  axcnre  7657  negid  7977  subneg  7979  negneg  7980  dfinfre  8682  2times  8816  infrenegsupex  9357  rexneg  9581  xaddpnf2  9598  xaddmnf1  9599  xaddmnf2  9600  fseq1p1m1  9842  fzosplitprm1  9979  intfracq  10061  frec2uz0d  10140  frec2uzrdg  10150  frecuzrdg0  10154  frecuzrdgg  10157  frecuzrdg0t  10163  seq3val  10199  seqvalcd  10200  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsum  10241  sqval  10319  iexpcyc  10365  binom3  10377  faclbnd  10455  faclbnd2  10456  bcn1  10472  hashinfom  10492  hashennn  10494  hashxp  10540  shftlem  10556  shftuz  10557  shftidt  10573  reim0  10601  remullem  10611  resqrexlemf1  10748  resqrexlemcalc3  10756  absexpzap  10820  absimle  10824  amgm2  10858  minmax  10969  xrmaxiflemval  10987  xrmaxadd  10998  infxrnegsupex  11000  xrminmax  11002  summodc  11120  fsum3  11124  sumsnf  11146  sumsns  11152  isumclim3  11160  isumge0  11167  fsump1i  11170  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fsumconst  11191  fsumiun  11214  hashrabrex  11218  hashuni  11219  binom11  11223  isumsplit  11228  geo2sum  11251  mertensabs  11274  efgt1p2  11328  efgt1p  11329  resinval  11349  recosval  11350  cosadd  11371  ef01bndlem  11390  eirraplem  11410  ialgr0  11652  algrp1  11654  eucalg  11667  phiprmpw  11825  phiprm  11826  ennnfonelem0  11845  ennnfonelemfun  11857  ennnfonelemf1  11858  ennnfonelemrn  11859  ctinfomlemom  11867  ndxid  11910  setsfun0  11922  setsresg  11924  setscom  11926  strslfv2d  11928  ressid2  11945  ressval2  11946  tgidm  12170  tgrest  12265  ssidcn  12306  txcnmpt  12369  txcn  12371  blres  12530  mopnval  12538  remetdval  12635  divccncfap  12673  cncfmet  12675  cncfcncntop  12676  cnplimcim  12732  cnplimclemr  12734  limccnpcntop  12740  limccnp2cntop  12742  dvexp  12771  sin0pilem1  12789  pilem3  12791  ef2kpi  12814  sin2pim  12821  cos2pim  12822  sinmpi  12823  cosmpi  12824  sinppi  12825  cosppi  12826  sinhalfpip  12828  sinhalfpim  12829  coshalfpip  12830  coshalfpim  12831  tangtx  12846  ex-ceil  12865  qdencn  13149  cvgcmp2nlemabs  13154  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator