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

Theorem eqeltrdi 2255
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 2241 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1342  wcel 2135
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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160
This theorem is referenced by:  eqeltrrdi  2256  snexprc  4160  onsucelsucexmidlem  4501  dcextest  4553  nnpredcl  4595  ovprc  5869  nnmcl  6441  xpsnen  6779  pw1fin  6868  xpfi  6887  snexxph  6907  ctssdclemn0  7067  nninfisollemne  7087  nninfisol  7089  exmidonfinlem  7141  pw1on  7174  indpi  7275  nq0m0r  7389  genpelxp  7444  un0mulcl  9140  znegcl  9214  zeo  9288  eqreznegel  9544  xnegcl  9760  modqid0  10276  q2txmodxeq0  10310  ser0  10440  expcllem  10457  m1expcl2  10468  nn0ltexp2  10613  bcval  10652  bccl  10670  hashinfom  10681  resqrexlemlo  10945  iserge0  11274  sumrbdclem  11308  fsum3cvg  11309  summodclem3  11311  summodclem2a  11312  fisumss  11323  binom  11415  bcxmas  11420  prodf1  11473  prodrbdclem  11502  fproddccvg  11503  prodmodclem2a  11507  fprodntrivap  11515  prodssdc  11520  fprodssdc  11521  gcdval  11881  gcdcl  11888  lcmcl  11993  pcxnn0cl  12231  pcxcl  12232  pcmptcl  12261  infpnlem2  12279  ssblps  12992  ssbl  12993  xmeter  13003  blssioo  13112  bj-charfun  13550  012of  13736  2o01f  13737  nninfsellemeqinf  13757  nninffeq  13761  trilpolemclim  13776  iswomni0  13791
  Copyright terms: Public domain W3C validator