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

Theorem 3eqtr4g 2197
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 2184 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2190 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  rabbidva2  2673  rabeqf  2676  csbeq1  3006  csbeq2  3026  csbeq2d  3027  csbnestgf  3052  difeq1  3187  difeq2  3188  uneq2  3224  ineq2  3271  dfrab3ss  3354  ifeq1  3477  ifeq2  3478  ifbi  3492  pweq  3513  sneq  3538  csbsng  3584  rabsn  3590  preq1  3600  preq2  3601  tpeq1  3609  tpeq2  3610  tpeq3  3611  prprc1  3631  opeq1  3705  opeq2  3706  oteq1  3714  oteq2  3715  oteq3  3716  csbunig  3744  unieq  3745  inteq  3774  iineq1  3827  iineq2  3830  dfiin2g  3846  iinrabm  3875  iinin1m  3882  iinxprg  3887  opabbid  3993  mpteq12f  4008  suceq  4324  xpeq1  4553  xpeq2  4554  csbxpg  4620  csbdmg  4733  rneq  4766  reseq1  4813  reseq2  4814  csbresg  4822  resindm  4861  resmpt  4867  resmptf  4869  imaeq1  4876  imaeq2  4877  mptcnv  4941  csbrng  5000  dmpropg  5011  rnpropg  5018  cores  5042  cores2  5051  xpcom  5085  iotaeq  5096  iotabi  5097  fntpg  5179  funimaexg  5207  fveq1  5420  fveq2  5421  fvres  5445  csbfv12g  5457  fnimapr  5481  fndmin  5527  fprg  5603  fsnunfv  5621  fsnunres  5622  fliftf  5700  isoini2  5720  riotaeqdv  5731  riotabidv  5732  riotauni  5736  riotabidva  5746  snriota  5759  oveq  5780  oveq1  5781  oveq2  5782  oprabbid  5824  mpoeq123  5830  mpoeq123dva  5832  mpoeq3dva  5835  resmpo  5869  ovres  5910  f1ocnvd  5972  ofeq  5984  ofreq  5985  f1od2  6132  ovtposg  6156  recseq  6203  tfr2a  6218  rdgeq1  6268  rdgeq2  6269  freceq1  6289  freceq2  6290  eceq1  6464  eceq2  6466  qseq1  6477  qseq2  6478  uniqs  6487  ecinxp  6504  qsinxp  6505  erovlem  6521  ixpeq1  6603  supeq1  6873  supeq2  6876  supeq3  6877  supeq123d  6878  infeq1  6898  infeq2  6901  infeq3  6902  infeq123d  6903  infisoti  6919  djueq12  6924  addpiord  7131  mulpiord  7132  00sr  7584  negeq  7962  csbnegg  7967  negsubdi  8025  mulneg1  8164  deceq1  9193  deceq2  9194  xnegeq  9617  fseq1p1m1  9881  frec2uzsucd  10181  frec2uzrdg  10189  frecuzrdgsuc  10194  frecuzrdgg  10196  frecuzrdgsuctlem  10203  seqeq1  10228  seqeq2  10229  seqeq3  10230  seqvalcd  10239  seq3f1olemp  10282  hashprg  10561  shftdm  10601  resqrexlemfp1  10788  negfi  11006  sumeq1  11131  sumeq2  11135  zsumdc  11160  isumss2  11169  fsumsplitsnun  11195  isumclim3  11199  fisumcom2  11214  isumshft  11266  prodeq1f  11328  prodeq2w  11332  prodeq2  11333  ege2le3  11384  efgt1p2  11408  dfphi2  11902  sloteq  11973  setsslid  12018  metreslem  12558  comet  12677  cnmetdval  12707
  Copyright terms: Public domain W3C validator