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

Theorem syl6eq 2133
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 2117 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  syl6req  2134  syl6eqr  2135  3eqtr3g  2140  3eqtr4a  2143  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  csbprc  3316  un00  3317  disjssun  3334  disjpr2  3489  tppreq3  3528  diftpsn3  3561  preq12b  3597  intsng  3705  uniintsnr  3707  rint0  3710  riin0  3784  iununir  3794  intexr  3960  sucprc  4212  op1stbg  4273  elreldm  4628  xpeq0r  4817  xpdisj1  4818  xpdisj2  4819  resdisj  4822  xpima1  4840  xpima2m  4841  elxp4  4881  unixp0im  4930  uniabio  4953  iotass  4960  cnvresid  5050  funimacnv  5052  f1o00  5245  dffv4g  5259  fnrnfv  5308  feqresmpt  5315  dffn5imf  5316  funfvdm2f  5326  fvun1  5327  fvmpt2  5343  fndmin  5363  fmptcof  5422  fmptcos  5423  fvunsng  5448  fvpr1  5456  fnrnov  5741  offval  5814  ofrfval  5815  op1std  5870  op2ndd  5871  fmpt2co  5932  tpostpos  5977  tfr0  6036  rdgival  6095  frec0g  6110  2oconcl  6151  om0  6167  oei0  6168  oasuc  6173  omv2  6174  nnm0r  6188  uniqs2  6298  en1  6462  en1bg  6463  fundmen  6469  mapsnen  6474  xpsnen  6483  xpcomco  6488  xpdom2  6493  xpmapenlem  6511  unsnfidcex  6576  ssfirab  6587  sbthlemi8  6610  djudom  6724  en2other2  6759  exmidfodomrlemim  6764  nq0m0r  6952  addpinq1  6960  genipv  7005  genpelvl  7008  genpelvu  7009  cauappcvgprlem1  7155  caucvgsrlemoffres  7282  addresr  7311  mulresr  7312  axcnre  7353  add20  7889  rimul  7996  rereim  7997  mulreim  8015  div4p1lem1div2  8595  nnm1nn0  8640  znegcl  8707  peano2z  8712  nneoor  8774  nn0ind-raph  8789  xnegneg  9220  xltnegi  9222  fzo0to2pr  9550  fldiv4p1lem1div2  9633  mulp1mod1  9693  frecfzennn  9754  iseqf1olemqk  9820  exp0  9850  expp1  9853  expnegap0  9854  1exp  9875  mulexp  9885  m1expeven  9893  sq0i  9937  bernneq  9963  facp1  10027  faclbnd3  10040  facubnd  10042  ibcval5  10060  hashinfom  10075  hashsng  10095  hashxp  10123  resunimafz0  10125  zfz1iso  10135  imre  10173  reim0b  10184  rereb  10185  resqrexlemover  10331  resqrexlemcalc1  10335  abs00bd  10387  maxabslemlub  10528  climconst  10564  isumz  10660  fsumf1o  10661  dvdsabseq  10715  odd2np1lem  10739  oddp1even  10743  opoe  10762  m1expo  10767  m1exp1  10768  nn0o1gt2  10772  gcddvds  10822  gcdcl  10825  gcdeq0  10835  gcd0id  10837  bezoutr1  10889  eucialg  10908  lcm0val  10914  lcmid  10929  rpmul  10947  dfphi2  11063  phiprmpw  11065  hashgcdeq  11071  ex-ceil  11084  bj-intexr  11229  peano3nninf  11327  nninfall  11330
  Copyright terms: Public domain W3C validator