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

Theorem 3eqtr4i 2148
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 2141 . 2  |-  D  =  A
51, 4eqtr4i 2141 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  rabswap  2586  rabbiia  2645  cbvrab  2658  cbvcsb  2979  csbco  2984  cbvrabcsf  3035  un4  3206  in13  3259  in31  3260  in4  3262  indifcom  3292  indir  3295  undir  3296  notrab  3323  dfnul3  3336  rab0  3361  prcom  3569  tprot  3586  tpcoma  3587  tpcomb  3588  tpass  3589  qdassr  3591  pw0  3637  opid  3693  int0  3755  cbviun  3820  cbviin  3821  iunrab  3830  iunin1  3847  cbvopab  3969  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab2v  3975  unopab  3977  cbvmptf  3992  cbvmpt  3993  iunopab  4173  uniuni  4342  2ordpr  4409  rabxp  4546  fconstmpt  4556  inxp  4643  cnvco  4694  rnmpt  4757  resundi  4802  resundir  4803  resindi  4804  resindir  4805  rescom  4814  resima  4822  imadmrn  4861  cnvimarndm  4873  cnvi  4913  rnun  4917  imaundi  4921  cnvxp  4927  imainrect  4954  imacnvcnv  4973  resdmres  5000  imadmres  5001  mptpreima  5002  cbviota  5063  sb8iota  5065  resdif  5357  cbvriota  5708  dfoprab2  5786  cbvoprab1  5811  cbvoprab2  5812  cbvoprab12  5813  cbvoprab3  5815  cbvmpox  5817  resoprab  5835  caov32  5926  caov31  5928  ofmres  6002  dfopab2  6055  dfxp3  6060  dmmpossx  6065  fmpox  6066  tposco  6140  mapsncnv  6557  cbvixp  6577  xpcomco  6688  sbthlemi6  6818  xp2dju  7039  djuassen  7041  dmaddpi  7101  dmmulpi  7102  dfplpq2  7130  dfmpq2  7131  dmaddpq  7155  dmmulpq  7156  axi2m1  7651  negiso  8677  nummac  9184  decsubi  9202  9t11e99  9269  fzprval  9817  fztpval  9818  sqdivapi  10331  binom2i  10356  4bc2eq6  10475  shftidt2  10559  cji  10629  xrnegiso  10986  cbvsum  11084  fsumrelem  11195  nn0gcdsq  11789  restco  12254  cnmptid  12361
  Copyright terms: Public domain W3C validator