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

Theorem 3eqtr4g 2113
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3eqtr4g.1  |-  ( ph  ->  A  =  B )
3eqtr4g.2  |-  C  =  A
3eqtr4g.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4g  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4g
StepHypRef Expression
1 3eqtr4g.2 . . 3  |-  C  =  A
2 3eqtr4g.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2syl5eq 2100 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2106 1  |-  ( ph  ->  C  =  D )
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:  rabeqf  2567  csbeq1  2883  csbeq2d  2902  csbnestgf  2926  difeq1  3083  difeq2  3084  uneq2  3119  ineq2  3160  dfrab3ss  3243  ifeq1  3362  ifeq2  3363  ifbi  3376  pweq  3390  sneq  3414  csbsng  3459  rabsn  3465  preq1  3475  preq2  3476  tpeq1  3484  tpeq2  3485  tpeq3  3486  prprc1  3506  opeq1  3577  opeq2  3578  oteq1  3586  oteq2  3587  oteq3  3588  csbunig  3616  unieq  3617  inteq  3646  iineq1  3699  iineq2  3702  dfiin2g  3718  iinrabm  3747  iinin1m  3754  iinxprg  3759  opabbid  3850  mpteq12f  3865  suceq  4167  xpeq1  4387  xpeq2  4388  csbxpg  4449  csbdmg  4557  rneq  4589  reseq1  4634  reseq2  4635  csbresg  4643  resmpt  4684  imaeq1  4691  imaeq2  4692  csbrng  4810  dmpropg  4821  rnpropg  4828  cores  4852  cores2  4861  xpcom  4892  iotaeq  4903  iotabi  4904  fntpg  4983  funimaexg  5011  fveq1  5205  fveq2  5206  fvres  5226  csbfv12g  5237  fnimapr  5261  fndmin  5302  fprg  5374  fsnunfv  5391  fsnunres  5392  fliftf  5467  isoini2  5486  riotaeqdv  5497  riotabidv  5498  riotauni  5502  riotabidva  5512  snriota  5525  oveq  5546  oveq1  5547  oveq2  5548  oprabbid  5586  mpt2eq123  5592  mpt2eq123dva  5594  mpt2eq3dva  5597  resmpt2  5627  ovres  5668  f1ocnvd  5730  ofeq  5742  ofreq  5743  f1od2  5884  ovtposg  5905  recseq  5952  tfr2a  5967  rdgeq1  5989  rdgeq2  5990  freceq1  6010  freceq2  6011  eceq1  6172  eceq2  6174  qseq1  6185  qseq2  6186  uniqs  6195  ecinxp  6212  qsinxp  6213  erovlem  6229  supeq1  6392  supeq2  6395  supeq3  6396  supeq123d  6397  addpiord  6472  mulpiord  6473  00sr  6912  negeq  7267  csbnegg  7272  negsubdi  7330  mulneg1  7464  deceq1  8431  deceq2  8432  xnegeq  8841  fseq1p1m1  9058  frec2uzzd  9350  frec2uzsucd  9351  frec2uzrdg  9359  frecuzrdgsuc  9365  iseqeq1  9378  iseqeq2  9379  iseqeq3  9380  iseqeq4  9381  shftdm  9651  resqrexlemfp1  9836  sumeq1  10105
  Copyright terms: Public domain W3C validator