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

Theorem eleqtrrdi 2233
Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
eleqtrrdi.1 (𝜑𝐴𝐵)
eleqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
eleqtrrdi (𝜑𝐴𝐶)

Proof of Theorem eleqtrrdi
StepHypRef Expression
1 eleqtrrdi.1 . 2 (𝜑𝐴𝐵)
2 eleqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2143 . 2 𝐵 = 𝐶
41, 3eleqtrdi 2232 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wcel 1480
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  brelrng  4770  elabrex  5659  fliftel1  5695  ovidig  5888  unielxp  6072  2oconcl  6336  ecopqsi  6484  eroprf  6522  sbthlem2  6846  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  caseinl  6976  caseinr  6977  ctssdccl  6996  isnumi  7038  addclnq  7190  mulclnq  7191  recexnq  7205  ltexnqq  7223  prarloclemarch  7233  prarloclemarch2  7234  nnnq  7237  nqnq0  7256  addclnq0  7266  mulclnq0  7267  nqpnq0nq  7268  prarloclemlt  7308  prarloclemlo  7309  prarloclemcalc  7317  nqprm  7357  cauappcvgprlem2  7475  caucvgprlem2  7495  addclsr  7568  mulclsr  7569  prsrcl  7599  mappsrprg  7619  suplocsrlemb  7621  pitonnlem2  7662  pitore  7665  recnnre  7666  axaddcl  7679  axmulcl  7681  axcaucvglemcl  7710  axcaucvglemval  7712  axcaucvglemcau  7713  axcaucvglemres  7714  uztrn2  9350  eluz2nn  9371  peano2uzs  9386  rebtwn2z  10039  seqf  10241  ser0  10294  bcm1k  10513  bcp1nk  10515  bcpasc  10519  hashennn  10533  hashcl  10534  climconst  11066  climshft2  11082  clim2ser  11113  clim2ser2  11114  iserex  11115  serf0  11128  zsumdc  11160  fsump1i  11209  iserabs  11251  isumshft  11266  isumsplit  11267  isum1p  11268  isumrpcl  11270  cvgratnnlemseq  11302  cvgratz  11308  cvgratgt0  11309  clim2prod  11315  clim2divap  11316  prodf1  11318  ntrivcvgap0  11325  ef0lem  11373  dvdsflip  11556  fzo0dvdseq  11562  gcdsupcl  11654  ialgr0  11732  prmind2  11808  crth  11907  ennnfonelemkh  11932  ennnfonelemrn  11939  ennnfonelemdm  11940  ctiunctlemf  11958  strslfv2d  12011  1strbas  12068  2strbasg  12070  2stropg  12071  2strbas1g  12073  rngbaseg  12085  rngplusgg  12086  rngmulrg  12087  srngbased  12092  srngplusgd  12093  srngmulrd  12094  srnginvld  12095  lmodbased  12103  lmodplusgd  12104  lmodscad  12105  lmodvscad  12106  ipsbased  12111  ipsaddgd  12112  ipsmulrd  12113  ipsscad  12114  ipsvscad  12115  ipsipd  12116  topgrpbasd  12121  topgrpplusgd  12122  topgrptsetd  12123  lmconst  12395  lmss  12425  uptx  12453  cnmpt1res  12475  dvidlemap  12839  dvrecap  12856  pilem3  12877  djulclALT  13038  djurclALT  13039  pwle2  13223  trilpolemeq1  13263
  Copyright terms: Public domain W3C validator