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

Theorem 3eqtr4i 2171
 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 2164 . 2
51, 4eqtr4i 2164 1
 Colors of variables: wff set class Syntax hints:   wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  rabswap  2613  rabbiia  2675  cbvrab  2688  cbvcsbw  3012  cbvcsb  3013  csbco  3018  cbvrabcsf  3071  un4  3242  in13  3295  in31  3296  in4  3298  indifcom  3328  indir  3331  undir  3332  notrab  3359  dfnul3  3372  rab0  3397  prcom  3608  tprot  3625  tpcoma  3626  tpcomb  3627  tpass  3628  qdassr  3630  pw0  3676  opid  3732  int0  3794  cbviun  3859  cbviin  3860  iunrab  3869  iunin1  3886  cbvopab  4008  cbvopab1  4010  cbvopab2  4011  cbvopab1s  4012  cbvopab2v  4014  unopab  4016  cbvmptf  4031  cbvmpt  4032  iunopab  4212  uniuni  4381  2ordpr  4448  rabxp  4585  fconstmpt  4595  inxp  4682  cnvco  4733  rnmpt  4796  resundi  4841  resundir  4842  resindi  4843  resindir  4844  rescom  4853  resima  4861  imadmrn  4900  cnvimarndm  4912  cnvi  4952  rnun  4956  imaundi  4960  cnvxp  4966  imainrect  4993  imacnvcnv  5012  resdmres  5039  imadmres  5040  mptpreima  5041  cbviota  5102  sb8iota  5104  resdif  5398  cbvriota  5749  dfoprab2  5827  cbvoprab1  5852  cbvoprab2  5853  cbvoprab12  5854  cbvoprab3  5856  cbvmpox  5858  resoprab  5876  caov32  5967  caov31  5969  ofmres  6043  dfopab2  6096  dfxp3  6101  dmmpossx  6106  fmpox  6107  tposco  6181  mapsncnv  6598  cbvixp  6618  xpcomco  6729  sbthlemi6  6860  xp2dju  7091  djuassen  7093  dmaddpi  7177  dmmulpi  7178  dfplpq2  7206  dfmpq2  7207  dmaddpq  7231  dmmulpq  7232  axi2m1  7727  negiso  8757  nummac  9270  decsubi  9288  9t11e99  9355  fzprval  9913  fztpval  9914  sqdivapi  10427  binom2i  10452  4bc2eq6  10572  shftidt2  10656  cji  10726  xrnegiso  11083  cbvsum  11181  fsumrelem  11292  cbvprod  11379  nn0gcdsq  11934  restco  12402  cnmptid  12509  sincos3rdpi  12992
 Copyright terms: Public domain W3C validator