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

Theorem eqeltrdi 2230
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrdi.1  |-  ( ph  ->  A  =  B )
eqeltrdi.2  |-  B  e.  C
Assertion
Ref Expression
eqeltrdi  |-  ( ph  ->  A  e.  C )

Proof of Theorem eqeltrdi
StepHypRef Expression
1 eqeltrdi.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeltrdi.2 . . 3  |-  B  e.  C
32a1i 9 . 2  |-  ( ph  ->  B  e.  C )
41, 3eqeltrd 2216 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. 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:  eqeltrrdi  2231  snexprc  4110  onsucelsucexmidlem  4444  dcextest  4495  nnpredcl  4536  ovprc  5806  nnmcl  6377  xpsnen  6715  xpfi  6818  snexxph  6838  ctssdclemn0  6995  exmidonfinlem  7049  indpi  7157  nq0m0r  7271  genpelxp  7326  un0mulcl  9018  znegcl  9092  zeo  9163  eqreznegel  9413  xnegcl  9622  modqid0  10130  q2txmodxeq0  10164  ser0  10294  expcllem  10311  m1expcl2  10322  bcval  10502  bccl  10520  hashinfom  10531  resqrexlemlo  10792  iserge0  11119  sumrbdclem  11153  fsum3cvg  11154  summodclem3  11156  summodclem2a  11157  fisumss  11168  binom  11260  bcxmas  11265  prodf1  11318  prodrbdclem  11347  fproddccvg  11348  prodmodclem2a  11352  gcdval  11655  gcdcl  11662  lcmcl  11760  ssblps  12604  ssbl  12605  xmeter  12615  blssioo  12724  nninfsellemeqinf  13242  nninffeq  13246  isomninnlem  13255  trilpolemclim  13259
  Copyright terms: Public domain W3C validator