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

Theorem 3eqtr4i 2113
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 2106 . 2  |-  D  =  A
51, 4eqtr4i 2106 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  rabswap  2538  rabbiia  2597  cbvrab  2610  cbvcsb  2923  csbco  2928  cbvrabcsf  2978  un4  3144  in13  3197  in31  3198  in4  3200  indifcom  3228  indir  3231  undir  3232  notrab  3259  dfnul3  3272  rab0  3294  prcom  3492  tprot  3509  tpcoma  3510  tpcomb  3511  tpass  3512  qdassr  3514  pw0  3558  opid  3614  int0  3676  cbviun  3741  cbviin  3742  iunrab  3751  iunin1  3768  cbvopab  3875  cbvopab1  3877  cbvopab2  3878  cbvopab1s  3879  cbvopab2v  3881  unopab  3883  cbvmpt  3898  iunopab  4072  uniuni  4237  2ordpr  4303  rabxp  4436  fconstmpt  4443  inxp  4528  cnvco  4579  rnmpt  4641  resundi  4684  resundir  4685  resindi  4686  resindir  4687  rescom  4695  resima  4702  imadmrn  4739  cnvimarndm  4751  cnvi  4790  rnun  4794  imaundi  4798  cnvxp  4804  imainrect  4830  imacnvcnv  4849  resdmres  4876  imadmres  4877  mptpreima  4878  cbviota  4939  sb8iota  4941  resdif  5223  cbvriota  5557  dfoprab2  5631  cbvoprab1  5655  cbvoprab2  5656  cbvoprab12  5657  cbvoprab3  5659  cbvmpt2x  5661  resoprab  5676  caov32  5767  caov31  5769  ofmres  5842  dfopab2  5894  dfxp3  5899  dmmpt2ssx  5904  fmpt2x  5905  tposco  5972  mapsncnv  6382  xpcomco  6472  dmaddpi  6787  dmmulpi  6788  dfplpq2  6816  dfmpq2  6817  dmaddpq  6841  dmmulpq  6842  axi2m1  7313  negiso  8310  nummac  8816  decsubi  8834  9t11e99  8901  fzprval  9389  fztpval  9390  sqdivapi  9875  binom2i  9899  4bc2eq6  10017  shftidt2  10094  cji  10163  nn0gcdsq  10958
  Copyright terms: Public domain W3C validator