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

Theorem 3eqtr4i 2070
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 𝐴 = 𝐵
3eqtr4i.2 𝐶 = 𝐴
3eqtr4i.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4i 𝐶 = 𝐷

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2 𝐶 = 𝐴
2 3eqtr4i.3 . . 3 𝐷 = 𝐵
3 3eqtr4i.1 . . 3 𝐴 = 𝐵
42, 3eqtr4i 2063 . 2 𝐷 = 𝐴
51, 4eqtr4i 2063 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1243
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  rabswap  2488  rabbiia  2547  cbvrab  2555  cbvcsb  2856  csbco  2861  cbvrabcsf  2911  un4  3103  in13  3150  in31  3151  in4  3153  indifcom  3183  indir  3186  undir  3187  notrab  3214  dfnul3  3227  rab0  3246  prcom  3446  tprot  3463  tpcoma  3464  tpcomb  3465  tpass  3466  qdassr  3468  pw0  3511  opid  3567  int0  3629  cbviun  3694  cbviin  3695  iunrab  3704  iunin1  3721  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  unopab  3836  cbvmpt  3851  iunopab  4018  uniuni  4183  2ordpr  4249  rabxp  4380  fconstmpt  4387  inxp  4470  cnvco  4520  rnmpt  4582  resundi  4625  resundir  4626  resindi  4627  resindir  4628  rescom  4636  resima  4643  imadmrn  4678  cnvimarndm  4689  cnvi  4728  rnun  4732  imaundi  4736  cnvxp  4742  imainrect  4766  imacnvcnv  4785  resdmres  4812  imadmres  4813  mptpreima  4814  cbviota  4872  sb8iota  4874  resdif  5148  cbvriota  5478  dfoprab2  5552  cbvoprab1  5576  cbvoprab2  5577  cbvoprab12  5578  cbvoprab3  5580  cbvmpt2x  5582  resoprab  5597  caov32  5688  caov31  5690  ofmres  5763  dfopab2  5815  dfxp3  5820  dmmpt2ssx  5825  fmpt2x  5826  tposco  5890  xpcomco  6300  dmaddpi  6421  dmmulpi  6422  dfplpq2  6450  dfmpq2  6451  dmaddpq  6475  dmmulpq  6476  axi2m1  6947  nummac  8397  fzprval  8942  fztpval  8943  sqdivapi  9311  binom2i  9334  shftidt2  9407  cji  9476
  Copyright terms: Public domain W3C validator