ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr4i GIF 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 𝐴 = 𝐵
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 2108 . 2 𝐷 = 𝐴
51, 4eqtr4i 2108 1 𝐶 = 𝐷
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  3501  tprot  3518  tpcoma  3519  tpcomb  3520  tpass  3521  qdassr  3523  pw0  3567  opid  3623  int0  3685  cbviun  3750  cbviin  3751  iunrab  3760  iunin1  3777  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab2v  3890  unopab  3892  cbvmptf  3907  cbvmpt  3908  iunopab  4082  uniuni  4247  2ordpr  4313  rabxp  4446  fconstmpt  4453  inxp  4538  cnvco  4589  rnmpt  4651  resundi  4694  resundir  4695  resindi  4696  resindir  4697  rescom  4705  resima  4712  imadmrn  4751  cnvimarndm  4763  cnvi  4802  rnun  4806  imaundi  4810  cnvxp  4816  imainrect  4842  imacnvcnv  4861  resdmres  4888  imadmres  4889  mptpreima  4890  cbviota  4951  sb8iota  4953  resdif  5238  cbvriota  5579  dfoprab2  5653  cbvoprab1  5677  cbvoprab2  5678  cbvoprab12  5679  cbvoprab3  5681  cbvmpt2x  5683  resoprab  5698  caov32  5789  caov31  5791  ofmres  5864  dfopab2  5916  dfxp3  5921  dmmpt2ssx  5926  fmpt2x  5927  tposco  5994  mapsncnv  6404  xpcomco  6494  sbthlemi6  6615  dmaddpi  6828  dmmulpi  6829  dfplpq2  6857  dfmpq2  6858  dmaddpq  6882  dmmulpq  6883  axi2m1  7354  negiso  8351  nummac  8853  decsubi  8871  9t11e99  8938  fzprval  9426  fztpval  9427  sqdivapi  9936  binom2i  9960  4bc2eq6  10078  shftidt2  10162  cji  10231  cbvsum  10639  nn0gcdsq  11053
  Copyright terms: Public domain W3C validator