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

Theorem 3eqtr4g 2079
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 2066 . 2 (φ𝐶 = B)
4 3eqtr4g.3 . 2 𝐷 = B
53, 4syl6eqr 2072 1 (φ𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  rabeqf  2528  csbeq1  2832  csbeq2d  2851  csbnestgf  2875  difeq1  3032  difeq2  3033  uneq2  3068  ineq2  3109  dfrab3ss  3192  ifeq1  3313  ifeq2  3314  ifbi  3325  pweq  3337  sneq  3361  csbsng  3405  rabsn  3411  preq1  3421  preq2  3422  tpeq1  3430  tpeq2  3431  tpeq3  3432  prprc1  3452  opeq1  3523  opeq2  3524  oteq1  3532  oteq2  3533  oteq3  3534  csbunig  3562  unieq  3563  inteq  3592  iineq1  3645  iineq2  3648  dfiin2g  3664  iinrabm  3693  iinin1m  3700  iinxprg  3705  opabbid  3796  mpteq12f  3811  suceq  4088  xpeq1  4286  xpeq2  4287  csbxpg  4348  csbdmg  4456  rneq  4488  reseq1  4533  reseq2  4534  csbresg  4542  resmpt  4583  imaeq1  4590  imaeq2  4591  csbrng  4709  dmpropg  4720  rnpropg  4727  cores  4751  cores2  4760  xpcom  4791  iotaeq  4802  iotabi  4803  fntpg  4881  funimaexg  4909  fveq1  5102  fveq2  5103  fvres  5123  csbfv12g  5134  fnimapr  5158  fndmin  5199  fprg  5271  fsnunfv  5288  fsnunres  5289  fliftf  5364  isoini2  5383  riotaeqdv  5394  riotabidv  5395  riotauni  5398  riotabidva  5408  snriota  5421  oveq  5442  oveq1  5443  oveq2  5444  oprabbid  5481  mpt2eq123  5487  mpt2eq123dva  5489  mpt2eq3dva  5492  resmpt2  5522  ovres  5563  f1ocnvd  5625  ofeq  5637  ofreq  5638  ovtposg  5796  recseq  5843  tfr2a  5858  rdgeq1  5879  rdgeq2  5880  eceq1  6052  eceq2  6054  qseq1  6065  qseq2  6066  uniqs  6075  ecinxp  6092  qsinxp  6093  erovlem  6109  addpiord  6176  mulpiord  6177  00sr  6516  negeq  6791  csbnegg  6796  negsubdi  6853  mulneg1  6978
  Copyright terms: Public domain W3C validator