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

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

Proof of Theorem syl6eleqr
StepHypRef Expression
1 syl6eleqr.1 . 2 (𝜑𝐴𝐵)
2 syl6eleqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2044 . 2 𝐵 = 𝐶
41, 3syl6eleq 2130 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  wcel 1393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036
This theorem is referenced by:  brelrng  4552  elabrex  5384  fliftel1  5421  ovidig  5605  unielxp  5787  2oconcl  6009  ecopqsi  6148  eroprf  6186  isnumi  6343  addclnq  6454  mulclnq  6455  recexnq  6469  ltexnqq  6487  prarloclemarch  6497  prarloclemarch2  6498  nnnq  6501  nqnq0  6520  addclnq0  6530  mulclnq0  6531  nqpnq0nq  6532  prarloclemlt  6572  prarloclemlo  6573  prarloclemcalc  6581  nqprm  6621  cauappcvgprlem2  6739  caucvgprlem2  6759  addclsr  6819  mulclsr  6820  prsrcl  6849  pitonnlem2  6904  pitore  6907  recnnre  6908  axaddcl  6921  axmulcl  6923  axcaucvglemcl  6950  axcaucvglemval  6952  axcaucvglemcau  6953  axcaucvglemres  6954  uztrn2  8462  eluz2nn  8483  peano2uzs  8499  iser0  9128  climconst  9688  climshft2  9704  clim2iser  9734  clim2iser2  9735  iiserex  9736  serif0  9748  ialgr0  9760
  Copyright terms: Public domain W3C validator