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

Theorem 3eqtr4i 2067
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 2060 . 2 𝐷 = A
51, 4eqtr4i 2060 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = 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:  rabswap  2482  rabbiia  2541  cbvrab  2549  cbvcsb  2850  csbco  2855  cbvrabcsf  2905  un4  3097  in13  3144  in31  3145  in4  3147  indifcom  3177  indir  3180  undir  3181  notrab  3208  dfnul3  3221  rab0  3240  prcom  3437  tprot  3454  tpcoma  3455  tpcomb  3456  tpass  3457  qdassr  3459  pw0  3502  opid  3558  int0  3620  cbviun  3685  cbviin  3686  iunrab  3695  iunin1  3712  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  unopab  3827  cbvmpt  3842  iunopab  4009  uniuni  4149  onsucelsucexmidlem  4214  rabxp  4323  fconstmpt  4330  inxp  4413  cnvco  4463  rnmpt  4525  resundi  4568  resundir  4569  resindi  4570  resindir  4571  rescom  4579  resima  4586  imadmrn  4621  cnvimarndm  4632  cnvi  4671  rnun  4675  imaundi  4679  cnvxp  4685  imainrect  4709  imacnvcnv  4728  resdmres  4755  imadmres  4756  mptpreima  4757  cbviota  4815  sb8iota  4817  resdif  5091  cbvriota  5421  dfoprab2  5494  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvoprab3  5522  cbvmpt2x  5524  resoprab  5539  caov32  5630  caov31  5632  ofmres  5705  dfopab2  5757  dfxp3  5762  dmmpt2ssx  5767  fmpt2x  5768  tposco  5831  xpcomco  6236  dmaddpi  6309  dmmulpi  6310  dfplpq2  6338  dfmpq2  6339  dmaddpq  6363  dmmulpq  6364  axi2m1  6739  nummac  8155  fzprval  8694  fztpval  8695  sqdivapi  8970  binom2i  8993  cji  9110
  Copyright terms: Public domain W3C validator