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

Theorem 3eqtr4i 2086
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 2079 . 2 𝐷 = 𝐴
51, 4eqtr4i 2079 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  rabswap  2505  rabbiia  2564  cbvrab  2572  cbvcsb  2884  csbco  2889  cbvrabcsf  2939  un4  3131  in13  3178  in31  3179  in4  3181  indifcom  3211  indir  3214  undir  3215  notrab  3242  dfnul3  3255  rab0  3274  prcom  3474  tprot  3491  tpcoma  3492  tpcomb  3493  tpass  3494  qdassr  3496  pw0  3539  opid  3595  int0  3657  cbviun  3722  cbviin  3723  iunrab  3732  iunin1  3749  cbvopab  3856  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  cbvopab2v  3862  unopab  3864  cbvmpt  3879  iunopab  4046  uniuni  4211  2ordpr  4277  rabxp  4408  fconstmpt  4415  inxp  4498  cnvco  4548  rnmpt  4610  resundi  4653  resundir  4654  resindi  4655  resindir  4656  rescom  4664  resima  4671  imadmrn  4706  cnvimarndm  4717  cnvi  4756  rnun  4760  imaundi  4764  cnvxp  4770  imainrect  4794  imacnvcnv  4813  resdmres  4840  imadmres  4841  mptpreima  4842  cbviota  4900  sb8iota  4902  resdif  5176  cbvriota  5506  dfoprab2  5580  cbvoprab1  5604  cbvoprab2  5605  cbvoprab12  5606  cbvoprab3  5608  cbvmpt2x  5610  resoprab  5625  caov32  5716  caov31  5718  ofmres  5791  dfopab2  5843  dfxp3  5848  dmmpt2ssx  5853  fmpt2x  5854  tposco  5921  xpcomco  6331  dmaddpi  6481  dmmulpi  6482  dfplpq2  6510  dfmpq2  6511  dmaddpq  6535  dmmulpq  6536  axi2m1  7007  nummac  8471  decsubi  8489  9t11e99  8556  fzprval  9046  fztpval  9047  sqdivapi  9503  binom2i  9527  4bc2eq6  9642  shftidt2  9661  cji  9730
  Copyright terms: Public domain W3C validator