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

Theorem 3eqtr4g 2142
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 2129 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2135 1  |-  ( ph  ->  C  =  D )
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:  rabbidva2  2602  rabeqf  2605  csbeq1  2925  csbeq2d  2944  csbnestgf  2969  difeq1  3100  difeq2  3101  uneq2  3137  ineq2  3184  dfrab3ss  3266  ifeq1  3382  ifeq2  3383  ifbi  3397  pweq  3418  sneq  3442  csbsng  3488  rabsn  3494  preq1  3504  preq2  3505  tpeq1  3513  tpeq2  3514  tpeq3  3515  prprc1  3535  opeq1  3607  opeq2  3608  oteq1  3616  oteq2  3617  oteq3  3618  csbunig  3646  unieq  3647  inteq  3676  iineq1  3729  iineq2  3732  dfiin2g  3748  iinrabm  3777  iinin1m  3784  iinxprg  3789  opabbid  3880  mpteq12f  3895  suceq  4205  xpeq1  4427  xpeq2  4428  csbxpg  4489  csbdmg  4600  rneq  4632  reseq1  4677  reseq2  4678  csbresg  4686  resindm  4723  resmpt  4729  resmptf  4731  imaeq1  4738  imaeq2  4739  csbrng  4860  dmpropg  4871  rnpropg  4878  cores  4902  cores2  4911  xpcom  4945  iotaeq  4956  iotabi  4957  fntpg  5037  funimaexg  5065  fveq1  5269  fveq2  5270  fvres  5294  csbfv12g  5305  fnimapr  5329  fndmin  5371  fprg  5445  fsnunfv  5462  fsnunres  5463  fliftf  5541  isoini2  5561  riotaeqdv  5572  riotabidv  5573  riotauni  5577  riotabidva  5587  snriota  5600  oveq  5621  oveq1  5622  oveq2  5623  oprabbid  5661  mpt2eq123  5667  mpt2eq123dva  5669  mpt2eq3dva  5672  resmpt2  5702  ovres  5743  f1ocnvd  5805  ofeq  5817  ofreq  5818  f1od2  5959  ovtposg  5980  recseq  6027  tfr2a  6042  rdgeq1  6092  rdgeq2  6093  freceq1  6113  freceq2  6114  eceq1  6281  eceq2  6283  qseq1  6294  qseq2  6295  uniqs  6304  ecinxp  6321  qsinxp  6322  erovlem  6338  supeq1  6628  supeq2  6631  supeq3  6632  supeq123d  6633  infeq1  6653  infeq2  6656  infeq3  6657  infeq123d  6658  infisoti  6674  djueq12  6679  addpiord  6822  mulpiord  6823  00sr  7262  negeq  7622  csbnegg  7627  negsubdi  7685  mulneg1  7820  deceq1  8816  deceq2  8817  xnegeq  9224  fseq1p1m1  9441  frec2uzsucd  9739  frec2uzrdg  9747  frecuzrdgsuc  9752  frecuzrdgg  9754  frecuzrdgsuctlem  9761  iseqeq1  9785  iseqeq2  9786  iseqeq3  9787  iseqeq4  9788  iseqf1olemp  9839  hashprg  10116  shftdm  10156  resqrexlemfp1  10341  negfi  10557  sumeq1  10639  sumeq2  10643  zisum  10668  isumss2  10676  fsumsplitsnun  10700  dfphi2  11102
  Copyright terms: Public domain W3C validator