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

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

Proof of Theorem eqeltrdi
StepHypRef Expression
1 eqeltrdi.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeltrdi.2 . . 3 𝐵𝐶
32a1i 9 . 2 (𝜑𝐵𝐶)
41, 3eqeltrd 2216 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:  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  11654  gcdcl  11661  lcmcl  11759  ssblps  12603  ssbl  12604  xmeter  12614  blssioo  12723  nninfsellemeqinf  13265  nninffeq  13269  isomninnlem  13278  trilpolemclim  13282
  Copyright terms: Public domain W3C validator