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

Theorem syl6eq 2104
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 2088 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  syl6req  2105  syl6eqr  2106  3eqtr3g  2111  3eqtr4a  2114  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  csbprc  3290  un00  3291  disjssun  3313  disjpr2  3462  tppreq3  3501  diftpsn3  3533  preq12b  3569  intsng  3677  uniintsnr  3679  rint0  3682  riin0  3756  iununir  3766  intexr  3932  sucprc  4177  op1stbg  4238  elreldm  4588  xpeq0r  4774  xpdisj1  4775  xpdisj2  4776  resdisj  4779  xpima1  4795  xpima2m  4796  elxp4  4836  unixp0im  4882  uniabio  4905  iotass  4912  cnvresid  5001  funimacnv  5003  f1o00  5189  dffv4g  5203  fnrnfv  5248  feqresmpt  5255  dffn5imf  5256  funfvdm2f  5266  fvun1  5267  fvmpt2  5282  fndmin  5302  fmptcof  5359  fmptcos  5360  fvunsng  5385  fvpr1  5393  fnrnov  5674  offval  5747  ofrfval  5748  op1std  5803  op2ndd  5804  fmpt2co  5865  tpostpos  5910  rdgival  6000  frec0g  6014  2oconcl  6053  om0  6069  oei0  6070  oasuc  6075  omv2  6076  nnm0r  6089  uniqs2  6197  en1  6310  en1bg  6311  fundmen  6317  xpsnen  6326  xpcomco  6331  xpdom2  6336  nq0m0r  6612  addpinq1  6620  genipv  6665  genpelvl  6668  genpelvu  6669  cauappcvgprlem1  6815  caucvgsrlemoffres  6942  addresr  6971  mulresr  6972  axcnre  7013  add20  7543  rimul  7650  rereim  7651  mulreim  7669  div4p1lem1div2  8235  nnm1nn0  8280  znegcl  8333  peano2z  8338  nneoor  8399  nn0ind-raph  8414  xnegneg  8847  xltnegi  8849  fzo0to2pr  9176  fldiv4p1lem1div2  9255  mulp1mod1  9315  frecfzennn  9367  exp0  9424  expp1  9427  expnegap0  9428  1exp  9449  mulexp  9459  m1expeven  9467  sq0i  9511  bernneq  9537  facp1  9598  faclbnd3  9611  facubnd  9613  ibcval5  9631  imre  9679  reim0b  9690  rereb  9691  resqrexlemover  9837  resqrexlemcalc1  9841  abs00bd  9893  climconst  10042  dvdsabseq  10159  odd2np1lem  10183  oddp1even  10187  opoe  10207  m1expo  10212  m1exp1  10213  nn0o1gt2  10217  ex-ceil  10280  bj-intexr  10415
  Copyright terms: Public domain W3C validator