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

Theorem eqeltrrid 2245
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrrid.1 𝐵 = 𝐴
eqeltrrid.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqeltrrid (𝜑𝐴𝐶)

Proof of Theorem eqeltrrid
StepHypRef Expression
1 eqeltrrid.1 . . 3 𝐵 = 𝐴
21eqcomi 2161 . 2 𝐴 = 𝐵
3 eqeltrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrid 2244 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1335  wcel 2128
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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153
This theorem is referenced by:  dmrnssfld  4851  cnvexg  5125  opabbrex  5867  offval  6041  resfunexgALT  6060  abrexexg  6068  abrexex2g  6070  opabex3d  6071  oprssdmm  6121  unfidisj  6868  ssfii  6920  djuexb  6990  nqprlu  7469  iccshftr  9904  iccshftl  9906  iccdil  9908  icccntr  9910  mertenslem2  11444  exprmfct  12030  ennnfonelemg  12202  0opn  12474  difopn  12578  tgrest  12639  txbasex  12727  txdis1cn  12748  cnmptid  12751  cnmptc  12752  cnmpt1st  12758  cnmpt2nd  12759  cnmpt2c  12760  hmeoima  12780  hmeocld  12782  fsumcncntop  13026
  Copyright terms: Public domain W3C validator