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

Theorem syl6eq 2186
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eq.1  |-  ( ph  ->  A  =  B )
syl6eq.2  |-  B  =  C
Assertion
Ref Expression
syl6eq  |-  ( ph  ->  A  =  C )

Proof of Theorem syl6eq
StepHypRef Expression
1 syl6eq.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eq.2 . . 3  |-  B  =  C
32a1i 9 . 2  |-  ( ph  ->  B  =  C )
41, 3eqtrd 2170 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
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:  syl6req  2187  syl6eqr  2188  3eqtr3g  2193  3eqtr4a  2196  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  csbprc  3403  un00  3404  disjssun  3421  disjpr2  3582  tppreq3  3621  diftpsn3  3656  preq12b  3692  intsng  3800  uniintsnr  3802  rint0  3805  riin0  3879  iununir  3891  intexr  4070  sucprc  4329  op1stbg  4395  elreldm  4760  xpeq0r  4956  xpdisj1  4958  xpdisj2  4959  resdisj  4962  xpima1  4980  xpima2m  4981  elxp4  5021  unixp0im  5070  uniabio  5093  iotass  5100  cnvresid  5192  funimacnv  5194  f1o00  5395  dffv4g  5411  fnrnfv  5461  feqresmpt  5468  dffn5imf  5469  funfvdm2f  5479  fvun1  5480  fvmpt2  5497  fndmin  5520  fmptcof  5580  fmptcos  5581  fvunsng  5607  fvpr1  5617  fnrnov  5909  offval  5982  ofrfval  5983  op1std  6039  op2ndd  6040  fmpoco  6106  tpostpos  6154  tfr0  6213  rdgival  6272  frec0g  6287  2oconcl  6329  om0  6347  oei0  6348  oasuc  6353  omv2  6354  nnm0r  6368  uniqs2  6482  en1  6686  en1bg  6687  fundmen  6693  mapsnen  6698  xpsnen  6708  xpcomco  6713  xpdom2  6718  xpmapenlem  6736  unsnfidcex  6801  fiintim  6810  ssfirab  6815  sbthlemi8  6845  elfi2  6853  fi0  6856  fieq0  6857  djudom  6971  ismkvnex  7022  en2other2  7045  exmidfodomrlemim  7050  nq0m0r  7257  addpinq1  7265  genipv  7310  genpelvl  7313  genpelvu  7314  cauappcvgprlem1  7460  caucvgsrlemoffres  7601  addresr  7638  mulresr  7639  axcnre  7682  add20  8229  rimul  8340  rereim  8341  mulreim  8359  sup3exmid  8708  fv0p1e1  8828  div4p1lem1div2  8966  nnm1nn0  9011  znegcl  9078  peano2z  9083  nneoor  9146  nn0ind-raph  9161  xnegneg  9609  xltnegi  9611  xaddpnf1  9622  xnegid  9635  xnn0xadd0  9643  xnegdi  9644  xsubge0  9657  xposdif  9658  xlesubadd  9659  xleaddadd  9663  fzo0to2pr  9988  fldiv4p1lem1div2  10071  mulp1mod1  10131  frecfzennn  10192  iseqf1olemqk  10260  exp0  10290  expp1  10293  expnegap0  10294  1exp  10315  mulexp  10325  m1expeven  10333  sq0i  10377  bernneq  10405  facp1  10469  faclbnd3  10482  facubnd  10484  bcval5  10502  hashinfom  10517  hashsng  10537  hashxp  10565  resunimafz0  10567  zfz1iso  10577  imre  10616  reim0b  10627  rereb  10628  resqrexlemover  10775  resqrexlemcalc1  10779  abs00bd  10831  maxabslemlub  10972  xrmaxiflemcom  11011  xrmaxadd  11023  climconst  11052  isumz  11151  fsumf1o  11152  fsumcllem  11161  fsumadd  11168  fsumxp  11198  fsumcnv  11199  fsummulc2  11210  fsumconst  11216  fsumabs  11227  telfsumo  11228  fsumparts  11232  fsumrelem  11233  fsumiun  11239  binomlem  11245  binom  11246  binom11  11248  isumsplit  11253  arisum  11260  arisum2  11261  trireciplem  11262  georeclim  11275  cvgratnnlemseq  11288  prodfrecap  11308  ef0lem  11355  ege2le3  11366  efaddlem  11369  efcan  11371  eft0val  11388  ef4p  11389  efgt1p2  11390  efi4p  11413  sincossq  11444  cos2tsin  11447  absefi  11464  demoivreALT  11469  dvdsabseq  11534  odd2np1lem  11558  oddp1even  11562  opoe  11581  m1expo  11586  m1exp1  11587  nn0o1gt2  11591  gcddvds  11641  gcdcl  11644  gcdeq0  11654  gcd0id  11656  bezoutr1  11710  eucalg  11729  lcm0val  11735  lcmid  11750  rpmul  11768  dfphi2  11885  phiprmpw  11887  hashgcdeq  11893  ennnfonelem0  11907  ennnfonelem1  11909  ennnfonelemhdmp1  11911  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemf1  11920  ctiunctlemfo  11941  setsresg  11986  strle1g  12038  restid2  12118  tgval2  12209  tgidm  12232  epttop  12248  tgrest  12327  restco  12332  restsn  12338  tgcn  12366  cnptopresti  12396  cnptoprest  12397  txbas  12416  upxp  12430  txrest  12434  txdis  12435  txhmeo  12477  txswaphmeolem  12478  xblss2ps  12562  xblss2  12563  qtopbasss  12679  fsumcncntop  12714  limcimolemlt  12791  dvcnp2cntop  12821  dvcoapbr  12829  dvexp  12833  dvexp2  12834  dveflem  12844  dvef  12845  sin0pilem1  12851  sin2kpi  12881  cos2kpi  12882  coseq0q4123  12904  coseq0negpitopi  12906  sincosq1eq  12909  sinkpi  12917  coskpi  12918  ex-ceil  12927  bj-intexr  13095  exmid1stab  13184  peano3nninf  13190  nninfall  13193  isomninnlem  13214
  Copyright terms: Public domain W3C validator