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

Theorem 3eqtr4g 2111
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 2098 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4g.3 . 2 𝐷 = 𝐵
53, 4syl6eqr 2104 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047
This theorem is referenced by:  rabeqf  2565  csbeq1  2880  csbeq2d  2899  csbnestgf  2923  difeq1  3080  difeq2  3081  uneq2  3116  ineq2  3157  dfrab3ss  3240  ifeq1  3359  ifeq2  3360  ifbi  3373  pweq  3387  sneq  3411  csbsng  3456  rabsn  3462  preq1  3472  preq2  3473  tpeq1  3481  tpeq2  3482  tpeq3  3483  prprc1  3503  opeq1  3574  opeq2  3575  oteq1  3583  oteq2  3584  oteq3  3585  csbunig  3613  unieq  3614  inteq  3643  iineq1  3696  iineq2  3699  dfiin2g  3715  iinrabm  3744  iinin1m  3751  iinxprg  3756  opabbid  3847  mpteq12f  3862  suceq  4164  xpeq1  4384  xpeq2  4385  csbxpg  4446  csbdmg  4554  rneq  4586  reseq1  4631  reseq2  4632  csbresg  4640  resmpt  4681  imaeq1  4688  imaeq2  4689  csbrng  4807  dmpropg  4818  rnpropg  4825  cores  4849  cores2  4858  xpcom  4889  iotaeq  4900  iotabi  4901  fntpg  4980  funimaexg  5008  fveq1  5202  fveq2  5203  fvres  5223  csbfv12g  5234  fnimapr  5258  fndmin  5299  fprg  5371  fsnunfv  5388  fsnunres  5389  fliftf  5464  isoini2  5483  riotaeqdv  5494  riotabidv  5495  riotauni  5499  riotabidva  5509  snriota  5522  oveq  5543  oveq1  5544  oveq2  5545  oprabbid  5583  mpt2eq123  5589  mpt2eq123dva  5591  mpt2eq3dva  5594  resmpt2  5624  ovres  5665  f1ocnvd  5727  ofeq  5739  ofreq  5740  f1od2  5881  ovtposg  5902  recseq  5949  tfr2a  5964  rdgeq1  5986  rdgeq2  5987  freceq1  6007  freceq2  6008  eceq1  6169  eceq2  6171  qseq1  6182  qseq2  6183  uniqs  6192  ecinxp  6209  qsinxp  6210  erovlem  6226  addpiord  6442  mulpiord  6443  00sr  6882  negeq  7237  csbnegg  7242  negsubdi  7300  mulneg1  7434  deceq1  8401  deceq2  8402  xnegeq  8811  fseq1p1m1  9028  frec2uzzd  9315  frec2uzsucd  9316  frec2uzrdg  9324  frecuzrdgsuc  9330  iseqeq1  9343  iseqeq2  9344  iseqeq3  9345  iseqeq4  9346  shftdm  9615  resqrexlemfp1  9799  sumeq1  10068
  Copyright terms: Public domain W3C validator