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

Theorem syl6eleqr 2147
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 2060 . 2 𝐵 = 𝐶
41, 3syl6eleq 2146 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  brelrng  4592  elabrex  5424  fliftel1  5461  ovidig  5645  unielxp  5827  2oconcl  6052  ecopqsi  6191  eroprf  6229  isnumi  6419  addclnq  6530  mulclnq  6531  recexnq  6545  ltexnqq  6563  prarloclemarch  6573  prarloclemarch2  6574  nnnq  6577  nqnq0  6596  addclnq0  6606  mulclnq0  6607  nqpnq0nq  6608  prarloclemlt  6648  prarloclemlo  6649  prarloclemcalc  6657  nqprm  6697  cauappcvgprlem2  6815  caucvgprlem2  6835  addclsr  6895  mulclsr  6896  prsrcl  6925  pitonnlem2  6980  pitore  6983  recnnre  6984  axaddcl  6997  axmulcl  6999  axcaucvglemcl  7026  axcaucvglemval  7028  axcaucvglemcau  7029  axcaucvglemres  7030  uztrn2  8585  eluz2nn  8606  peano2uzs  8622  rebtwn2z  9210  iser0  9414  bcm1k  9627  bcp1nk  9629  bcpasc  9633  climconst  10041  climshft2  10057  clim2iser  10087  clim2iser2  10088  iiserex  10089  serif0  10101  dvdsflip  10162  fzo0dvdseq  10168  ialgr0  10245
  Copyright terms: Public domain W3C validator