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

Theorem 3eqtr4g 2175
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 2162 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2168 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  rabbidva2  2647  rabeqf  2650  csbeq1  2978  csbeq2d  2997  csbnestgf  3022  difeq1  3157  difeq2  3158  uneq2  3194  ineq2  3241  dfrab3ss  3324  ifeq1  3447  ifeq2  3448  ifbi  3462  pweq  3483  sneq  3508  csbsng  3554  rabsn  3560  preq1  3570  preq2  3571  tpeq1  3579  tpeq2  3580  tpeq3  3581  prprc1  3601  opeq1  3675  opeq2  3676  oteq1  3684  oteq2  3685  oteq3  3686  csbunig  3714  unieq  3715  inteq  3744  iineq1  3797  iineq2  3800  dfiin2g  3816  iinrabm  3845  iinin1m  3852  iinxprg  3857  opabbid  3963  mpteq12f  3978  suceq  4294  xpeq1  4523  xpeq2  4524  csbxpg  4590  csbdmg  4703  rneq  4736  reseq1  4783  reseq2  4784  csbresg  4792  resindm  4831  resmpt  4837  resmptf  4839  imaeq1  4846  imaeq2  4847  mptcnv  4911  csbrng  4970  dmpropg  4981  rnpropg  4988  cores  5012  cores2  5021  xpcom  5055  iotaeq  5066  iotabi  5067  fntpg  5149  funimaexg  5177  fveq1  5388  fveq2  5389  fvres  5413  csbfv12g  5425  fnimapr  5449  fndmin  5495  fprg  5571  fsnunfv  5589  fsnunres  5590  fliftf  5668  isoini2  5688  riotaeqdv  5699  riotabidv  5700  riotauni  5704  riotabidva  5714  snriota  5727  oveq  5748  oveq1  5749  oveq2  5750  oprabbid  5792  mpoeq123  5798  mpoeq123dva  5800  mpoeq3dva  5803  resmpo  5837  ovres  5878  f1ocnvd  5940  ofeq  5952  ofreq  5953  f1od2  6100  ovtposg  6124  recseq  6171  tfr2a  6186  rdgeq1  6236  rdgeq2  6237  freceq1  6257  freceq2  6258  eceq1  6432  eceq2  6434  qseq1  6445  qseq2  6446  uniqs  6455  ecinxp  6472  qsinxp  6473  erovlem  6489  ixpeq1  6571  supeq1  6841  supeq2  6844  supeq3  6845  supeq123d  6846  infeq1  6866  infeq2  6869  infeq3  6870  infeq123d  6871  infisoti  6887  djueq12  6892  addpiord  7092  mulpiord  7093  00sr  7545  negeq  7923  csbnegg  7928  negsubdi  7986  mulneg1  8125  deceq1  9154  deceq2  9155  xnegeq  9578  fseq1p1m1  9842  frec2uzsucd  10142  frec2uzrdg  10150  frecuzrdgsuc  10155  frecuzrdgg  10157  frecuzrdgsuctlem  10164  seqeq1  10189  seqeq2  10190  seqeq3  10191  seqvalcd  10200  seq3f1olemp  10243  hashprg  10522  shftdm  10562  resqrexlemfp1  10749  negfi  10967  sumeq1  11092  sumeq2  11096  zsumdc  11121  isumss2  11130  fsumsplitsnun  11156  isumclim3  11160  fisumcom2  11175  isumshft  11227  ege2le3  11304  efgt1p2  11328  dfphi2  11823  sloteq  11891  setsslid  11936  metreslem  12476  comet  12595  cnmetdval  12625
  Copyright terms: Public domain W3C validator