ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr4g GIF 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 (𝜑𝐴 = 𝐵)
3eqtr4g.2 𝐶 = 𝐴
3eqtr4g.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4g (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr4g
StepHypRef Expression
1 3eqtr4g.2 . . 3 𝐶 = 𝐴
2 3eqtr4g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2syl5eq 2129 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2135 1 (𝜑𝐶 = 𝐷)
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  3486  rabsn  3492  preq1  3502  preq2  3503  tpeq1  3511  tpeq2  3512  tpeq3  3513  prprc1  3533  opeq1  3605  opeq2  3606  oteq1  3614  oteq2  3615  oteq3  3616  csbunig  3644  unieq  3645  inteq  3674  iineq1  3727  iineq2  3730  dfiin2g  3746  iinrabm  3775  iinin1m  3782  iinxprg  3787  opabbid  3878  mpteq12f  3893  suceq  4203  xpeq1  4425  xpeq2  4426  csbxpg  4487  csbdmg  4598  rneq  4630  reseq1  4675  reseq2  4676  csbresg  4684  resindm  4721  resmpt  4727  resmptf  4729  imaeq1  4736  imaeq2  4737  csbrng  4858  dmpropg  4869  rnpropg  4876  cores  4900  cores2  4909  xpcom  4943  iotaeq  4954  iotabi  4955  fntpg  5035  funimaexg  5063  fveq1  5267  fveq2  5268  fvres  5292  csbfv12g  5303  fnimapr  5327  fndmin  5369  fprg  5443  fsnunfv  5460  fsnunres  5461  fliftf  5539  isoini2  5559  riotaeqdv  5570  riotabidv  5571  riotauni  5575  riotabidva  5585  snriota  5598  oveq  5619  oveq1  5620  oveq2  5621  oprabbid  5659  mpt2eq123  5665  mpt2eq123dva  5667  mpt2eq3dva  5670  resmpt2  5700  ovres  5741  f1ocnvd  5803  ofeq  5815  ofreq  5816  f1od2  5957  ovtposg  5978  recseq  6025  tfr2a  6040  rdgeq1  6090  rdgeq2  6091  freceq1  6111  freceq2  6112  eceq1  6279  eceq2  6281  qseq1  6292  qseq2  6293  uniqs  6302  ecinxp  6319  qsinxp  6320  erovlem  6336  supeq1  6625  supeq2  6628  supeq3  6629  supeq123d  6630  infeq1  6650  infeq2  6653  infeq3  6654  infeq123d  6655  infisoti  6671  djueq12  6676  addpiord  6819  mulpiord  6820  00sr  7259  negeq  7619  csbnegg  7624  negsubdi  7682  mulneg1  7817  deceq1  8813  deceq2  8814  xnegeq  9221  fseq1p1m1  9438  frec2uzsucd  9736  frec2uzrdg  9744  frecuzrdgsuc  9749  frecuzrdgg  9751  frecuzrdgsuctlem  9758  iseqeq1  9782  iseqeq2  9783  iseqeq3  9784  iseqeq4  9785  iseqf1olemp  9836  hashprg  10113  shftdm  10153  resqrexlemfp1  10338  negfi  10554  sumeq1  10636  sumeq2  10640  zisum  10665  isumss2  10673  dfphi2  11078
  Copyright terms: Public domain W3C validator