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

Theorem 3eqtr4i 2115
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  |-  C  =  A
3eqtr4i.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4i  |-  C  =  D

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2  |-  C  =  A
2 3eqtr4i.3 . . 3  |-  D  =  B
3 3eqtr4i.1 . . 3  |-  A  =  B
42, 3eqtr4i 2108 . 2  |-  D  =  A
51, 4eqtr4i 2108 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  rabswap  2541  rabbiia  2600  cbvrab  2613  cbvcsb  2926  csbco  2931  cbvrabcsf  2982  un4  3149  in13  3202  in31  3203  in4  3205  indifcom  3234  indir  3237  undir  3238  notrab  3265  dfnul3  3278  rab0  3300  prcom  3503  tprot  3520  tpcoma  3521  tpcomb  3522  tpass  3523  qdassr  3525  pw0  3569  opid  3625  int0  3687  cbviun  3752  cbviin  3753  iunrab  3762  iunin1  3779  cbvopab  3886  cbvopab1  3888  cbvopab2  3889  cbvopab1s  3890  cbvopab2v  3892  unopab  3894  cbvmptf  3909  cbvmpt  3910  iunopab  4084  uniuni  4249  2ordpr  4315  rabxp  4448  fconstmpt  4455  inxp  4540  cnvco  4591  rnmpt  4653  resundi  4696  resundir  4697  resindi  4698  resindir  4699  rescom  4707  resima  4714  imadmrn  4753  cnvimarndm  4765  cnvi  4804  rnun  4808  imaundi  4812  cnvxp  4818  imainrect  4844  imacnvcnv  4863  resdmres  4890  imadmres  4891  mptpreima  4892  cbviota  4953  sb8iota  4955  resdif  5240  cbvriota  5581  dfoprab2  5655  cbvoprab1  5679  cbvoprab2  5680  cbvoprab12  5681  cbvoprab3  5683  cbvmpt2x  5685  resoprab  5700  caov32  5791  caov31  5793  ofmres  5866  dfopab2  5918  dfxp3  5923  dmmpt2ssx  5928  fmpt2x  5929  tposco  5996  mapsncnv  6406  xpcomco  6496  sbthlemi6  6618  dmaddpi  6831  dmmulpi  6832  dfplpq2  6860  dfmpq2  6861  dmaddpq  6885  dmmulpq  6886  axi2m1  7357  negiso  8354  nummac  8856  decsubi  8874  9t11e99  8941  fzprval  9429  fztpval  9430  sqdivapi  9958  binom2i  9982  4bc2eq6  10100  shftidt2  10184  cji  10253  cbvsum  10663  nn0gcdsq  11103
  Copyright terms: Public domain W3C validator