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

Theorem 3eqtr4g 2094
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3eqtr4g.1 (φA = B)
3eqtr4g.2 𝐶 = A
3eqtr4g.3 𝐷 = B
Assertion
Ref Expression
3eqtr4g (φ𝐶 = 𝐷)

Proof of Theorem 3eqtr4g
StepHypRef Expression
1 3eqtr4g.2 . . 3 𝐶 = A
2 3eqtr4g.1 . . 3 (φA = B)
31, 2syl5eq 2081 . 2 (φ𝐶 = B)
4 3eqtr4g.3 . 2 𝐷 = B
53, 4syl6eqr 2087 1 (φ𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  rabeqf  2544  csbeq1  2849  csbeq2d  2868  csbnestgf  2892  difeq1  3049  difeq2  3050  uneq2  3085  ineq2  3126  dfrab3ss  3209  ifeq1  3328  ifeq2  3329  ifbi  3342  pweq  3354  sneq  3378  csbsng  3422  rabsn  3428  preq1  3438  preq2  3439  tpeq1  3447  tpeq2  3448  tpeq3  3449  prprc1  3469  opeq1  3540  opeq2  3541  oteq1  3549  oteq2  3550  oteq3  3551  csbunig  3579  unieq  3580  inteq  3609  iineq1  3662  iineq2  3665  dfiin2g  3681  iinrabm  3710  iinin1m  3717  iinxprg  3722  opabbid  3813  mpteq12f  3828  suceq  4105  xpeq1  4302  xpeq2  4303  csbxpg  4364  csbdmg  4472  rneq  4504  reseq1  4549  reseq2  4550  csbresg  4558  resmpt  4599  imaeq1  4606  imaeq2  4607  csbrng  4725  dmpropg  4736  rnpropg  4743  cores  4767  cores2  4776  xpcom  4807  iotaeq  4818  iotabi  4819  fntpg  4898  funimaexg  4926  fveq1  5120  fveq2  5121  fvres  5141  csbfv12g  5152  fnimapr  5176  fndmin  5217  fprg  5289  fsnunfv  5306  fsnunres  5307  fliftf  5382  isoini2  5401  riotaeqdv  5412  riotabidv  5413  riotauni  5417  riotabidva  5427  snriota  5440  oveq  5461  oveq1  5462  oveq2  5463  oprabbid  5500  mpt2eq123  5506  mpt2eq123dva  5508  mpt2eq3dva  5511  resmpt2  5541  ovres  5582  f1ocnvd  5644  ofeq  5656  ofreq  5657  ovtposg  5815  recseq  5862  tfr2a  5877  rdgeq1  5898  rdgeq2  5899  freceq1  5919  freceq2  5920  eceq1  6077  eceq2  6079  qseq1  6090  qseq2  6091  uniqs  6100  ecinxp  6117  qsinxp  6118  erovlem  6134  addpiord  6300  mulpiord  6301  00sr  6697  negeq  7001  csbnegg  7006  negsubdi  7063  mulneg1  7188  deceq1  8146  deceq2  8147  xnegeq  8510  fseq1p1m1  8726  frec2uzzd  8867  frec2uzsucd  8868  frec2uzrdg  8876  frecuzrdgsuc  8882  iseqeq1  8894  iseqeq2  8895  iseqeq3  8896  iseqeq4  8897
  Copyright terms: Public domain W3C validator