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

Theorem 3eqtr4i 2171
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1 𝐴 = 𝐵
3eqtr4i.2 𝐶 = 𝐴
3eqtr4i.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4i 𝐶 = 𝐷

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2 𝐶 = 𝐴
2 3eqtr4i.3 . . 3 𝐷 = 𝐵
3 3eqtr4i.1 . . 3 𝐴 = 𝐵
42, 3eqtr4i 2164 . 2 𝐷 = 𝐴
51, 4eqtr4i 2164 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  rabswap  2612  rabbiia  2674  cbvrab  2687  cbvcsbw  3010  cbvcsb  3011  csbco  3016  cbvrabcsf  3069  un4  3240  in13  3293  in31  3294  in4  3296  indifcom  3326  indir  3329  undir  3330  notrab  3357  dfnul3  3370  rab0  3395  prcom  3606  tprot  3623  tpcoma  3624  tpcomb  3625  tpass  3626  qdassr  3628  pw0  3674  opid  3730  int0  3792  cbviun  3857  cbviin  3858  iunrab  3867  iunin1  3884  cbvopab  4006  cbvopab1  4008  cbvopab2  4009  cbvopab1s  4010  cbvopab2v  4012  unopab  4014  cbvmptf  4029  cbvmpt  4030  iunopab  4210  uniuni  4379  2ordpr  4446  rabxp  4583  fconstmpt  4593  inxp  4680  cnvco  4731  rnmpt  4794  resundi  4839  resundir  4840  resindi  4841  resindir  4842  rescom  4851  resima  4859  imadmrn  4898  cnvimarndm  4910  cnvi  4950  rnun  4954  imaundi  4958  cnvxp  4964  imainrect  4991  imacnvcnv  5010  resdmres  5037  imadmres  5038  mptpreima  5039  cbviota  5100  sb8iota  5102  resdif  5396  cbvriota  5747  dfoprab2  5825  cbvoprab1  5850  cbvoprab2  5851  cbvoprab12  5852  cbvoprab3  5854  cbvmpox  5856  resoprab  5874  caov32  5965  caov31  5967  ofmres  6041  dfopab2  6094  dfxp3  6099  dmmpossx  6104  fmpox  6105  tposco  6179  mapsncnv  6596  cbvixp  6616  xpcomco  6727  sbthlemi6  6857  xp2dju  7087  djuassen  7089  dmaddpi  7156  dmmulpi  7157  dfplpq2  7185  dfmpq2  7186  dmaddpq  7210  dmmulpq  7211  axi2m1  7706  negiso  8736  nummac  9249  decsubi  9267  9t11e99  9334  fzprval  9892  fztpval  9893  sqdivapi  10406  binom2i  10431  4bc2eq6  10551  shftidt2  10635  cji  10705  xrnegiso  11062  cbvsum  11160  fsumrelem  11271  cbvprod  11358  nn0gcdsq  11912  restco  12380  cnmptid  12487  sincos3rdpi  12970
  Copyright terms: Public domain W3C validator