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

Theorem 3eqtr4g 2152
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 2139 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2145 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-cleq 2088
This theorem is referenced by:  rabbidva2  2620  rabeqf  2623  csbeq1  2950  csbeq2d  2969  csbnestgf  2994  difeq1  3126  difeq2  3127  uneq2  3163  ineq2  3210  dfrab3ss  3293  ifeq1  3416  ifeq2  3417  ifbi  3431  pweq  3452  sneq  3477  csbsng  3523  rabsn  3529  preq1  3539  preq2  3540  tpeq1  3548  tpeq2  3549  tpeq3  3550  prprc1  3570  opeq1  3644  opeq2  3645  oteq1  3653  oteq2  3654  oteq3  3655  csbunig  3683  unieq  3684  inteq  3713  iineq1  3766  iineq2  3769  dfiin2g  3785  iinrabm  3814  iinin1m  3821  iinxprg  3826  opabbid  3925  mpteq12f  3940  suceq  4253  xpeq1  4481  xpeq2  4482  csbxpg  4548  csbdmg  4661  rneq  4694  reseq1  4739  reseq2  4740  csbresg  4748  resindm  4787  resmpt  4793  resmptf  4795  imaeq1  4802  imaeq2  4803  mptcnv  4867  csbrng  4926  dmpropg  4937  rnpropg  4944  cores  4968  cores2  4977  xpcom  5011  iotaeq  5022  iotabi  5023  fntpg  5104  funimaexg  5132  fveq1  5339  fveq2  5340  fvres  5364  csbfv12g  5375  fnimapr  5399  fndmin  5445  fprg  5519  fsnunfv  5537  fsnunres  5538  fliftf  5616  isoini2  5636  riotaeqdv  5647  riotabidv  5648  riotauni  5652  riotabidva  5662  snriota  5675  oveq  5696  oveq1  5697  oveq2  5698  oprabbid  5740  mpt2eq123  5746  mpt2eq123dva  5748  mpt2eq3dva  5751  resmpt2  5781  ovres  5822  f1ocnvd  5884  ofeq  5896  ofreq  5897  f1od2  6038  ovtposg  6062  recseq  6109  tfr2a  6124  rdgeq1  6174  rdgeq2  6175  freceq1  6195  freceq2  6196  eceq1  6367  eceq2  6369  qseq1  6380  qseq2  6381  uniqs  6390  ecinxp  6407  qsinxp  6408  erovlem  6424  ixpeq1  6506  supeq1  6761  supeq2  6764  supeq3  6765  supeq123d  6766  infeq1  6786  infeq2  6789  infeq3  6790  infeq123d  6791  infisoti  6807  djueq12  6812  addpiord  6972  mulpiord  6973  00sr  7412  negeq  7772  csbnegg  7777  negsubdi  7835  mulneg1  7970  deceq1  8980  deceq2  8981  xnegeq  9393  fseq1p1m1  9657  frec2uzsucd  9957  frec2uzrdg  9965  frecuzrdgsuc  9970  frecuzrdgg  9972  frecuzrdgsuctlem  9979  iseqeq3  10006  seqeq1  10007  seqeq2  10008  seqeq3  10009  seq3f1olemp  10068  hashprg  10347  shftdm  10387  resqrexlemfp1  10573  negfi  10790  sumeq1  10913  sumeq2  10917  zsumdc  10942  isumss2  10951  fsumsplitsnun  10977  isumclim3  10981  fisumcom2  10996  isumshft  11048  ege2le3  11125  efgt1p2  11149  dfphi2  11638  sloteq  11663  setsslid  11708  metreslem  12181  comet  12300  cnmetdval  12323
  Copyright terms: Public domain W3C validator