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

Theorem 3eqtr4g 2139
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 2126 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2132 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  rabeqf  2595  csbeq1  2912  csbeq2d  2931  csbnestgf  2955  difeq1  3084  difeq2  3085  uneq2  3121  ineq2  3168  dfrab3ss  3249  ifeq1  3362  ifeq2  3363  ifbi  3377  pweq  3393  sneq  3417  csbsng  3461  rabsn  3467  preq1  3477  preq2  3478  tpeq1  3486  tpeq2  3487  tpeq3  3488  prprc1  3508  opeq1  3578  opeq2  3579  oteq1  3587  oteq2  3588  oteq3  3589  csbunig  3617  unieq  3618  inteq  3647  iineq1  3700  iineq2  3703  dfiin2g  3719  iinrabm  3748  iinin1m  3755  iinxprg  3760  opabbid  3851  mpteq12f  3866  suceq  4165  xpeq1  4385  xpeq2  4386  csbxpg  4447  csbdmg  4557  rneq  4589  reseq1  4634  reseq2  4635  csbresg  4643  resindm  4680  resmpt  4686  imaeq1  4693  imaeq2  4694  csbrng  4812  dmpropg  4823  rnpropg  4830  cores  4854  cores2  4863  xpcom  4894  iotaeq  4905  iotabi  4906  fntpg  4986  funimaexg  5014  fveq1  5208  fveq2  5209  fvres  5230  csbfv12g  5241  fnimapr  5265  fndmin  5306  fprg  5378  fsnunfv  5395  fsnunres  5396  fliftf  5470  isoini2  5489  riotaeqdv  5500  riotabidv  5501  riotauni  5505  riotabidva  5515  snriota  5528  oveq  5549  oveq1  5550  oveq2  5551  oprabbid  5589  mpt2eq123  5595  mpt2eq123dva  5597  mpt2eq3dva  5600  resmpt2  5630  ovres  5671  f1ocnvd  5733  ofeq  5745  ofreq  5746  f1od2  5887  ovtposg  5908  recseq  5955  tfr2a  5970  rdgeq1  6020  rdgeq2  6021  freceq1  6041  freceq2  6042  eceq1  6207  eceq2  6209  qseq1  6220  qseq2  6221  uniqs  6230  ecinxp  6247  qsinxp  6248  erovlem  6264  supeq1  6458  supeq2  6461  supeq3  6462  supeq123d  6463  infeq1  6483  infeq2  6486  infeq3  6487  infeq123d  6488  infisoti  6504  addpiord  6568  mulpiord  6569  00sr  7008  negeq  7368  csbnegg  7373  negsubdi  7431  mulneg1  7566  deceq1  8562  deceq2  8563  xnegeq  8970  fseq1p1m1  9187  frec2uzsucd  9483  frec2uzrdg  9491  frecuzrdgsuc  9496  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqeq1  9524  iseqeq2  9525  iseqeq3  9526  iseqeq4  9527  sizeprg  9832  shftdm  9848  resqrexlemfp1  10033  negfi  10248  sumeq1  10330  sumeq2d  10334  sumeq2  10335
  Copyright terms: Public domain W3C validator