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

Theorem 3eqtr4i 2052
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 A = B
3eqtr4i.2 𝐶 = A
3eqtr4i.3 𝐷 = B
Assertion
Ref Expression
3eqtr4i 𝐶 = 𝐷

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2 𝐶 = A
2 3eqtr4i.3 . . 3 𝐷 = B
3 3eqtr4i.1 . . 3 A = B
42, 3eqtr4i 2045 . 2 𝐷 = A
51, 4eqtr4i 2045 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = 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:  rabswap  2466  rabbiia  2525  cbvrab  2533  cbvcsb  2833  csbco  2838  cbvrabcsf  2888  un4  3080  in13  3127  in31  3128  in4  3130  indifcom  3160  indir  3163  undir  3164  notrab  3191  dfnul3  3204  rab0  3223  prcom  3420  tprot  3437  tpcoma  3438  tpcomb  3439  tpass  3440  qdassr  3442  pw0  3485  opid  3541  int0  3603  cbviun  3668  cbviin  3669  iunrab  3678  iunin1  3695  cbvopab  3802  cbvopab1  3804  cbvopab2  3805  cbvopab1s  3806  cbvopab2v  3808  unopab  3810  cbvmpt  3825  iunopab  3992  uniuni  4133  onsucelsucexmidlem  4198  rabxp  4307  fconstmpt  4314  inxp  4397  cnvco  4447  rnmpt  4509  resundi  4552  resundir  4553  resindi  4554  resindir  4555  rescom  4563  resima  4570  imadmrn  4605  cnvimarndm  4616  cnvi  4655  rnun  4659  imaundi  4663  cnvxp  4669  imainrect  4693  imacnvcnv  4712  resdmres  4739  imadmres  4740  mptpreima  4741  cbviota  4799  sb8iota  4801  resdif  5073  cbvriota  5402  dfoprab2  5475  cbvoprab1  5499  cbvoprab2  5500  cbvoprab12  5501  cbvoprab3  5503  cbvmpt2x  5505  resoprab  5520  caov32  5611  caov31  5613  ofmres  5686  dfopab2  5738  dfxp3  5743  dmmpt2ssx  5748  fmpt2x  5749  tposco  5812  dmaddpi  6185  dmmulpi  6186  dfplpq2  6213  dfmpq2  6214  dmaddpq  6238  dmmulpq  6239  axi2m1  6569
  Copyright terms: Public domain W3C validator