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

Theorem eleq12d 2188
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1d.1 (𝜑𝐴 = 𝐵)
eleq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
eleq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3 (𝜑𝐶 = 𝐷)
21eleq2d 2187 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq1d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2186 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 187 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316  wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  cbvraldva2  2635  cbvrexdva2  2636  cdeqel  2878  ru  2881  sbcel12g  2988  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  onintexmid  4457  elvvuni  4573  elrnmpt1  4760  smoeq  6155  smores  6157  smores2  6159  iordsmo  6162  nnaordi  6372  nnaordr  6374  fvixp  6565  cbvixp  6577  mptelixpg  6596  exmidaclem  7032  ltapig  7114  ltmpig  7115  fzsubel  9808  elfzp1b  9845  ennnfonelemg  11843  ennnfonelemp1  11846  ennnfonelemnn0  11862  ctiunctlemu1st  11874  ctiunctlemu2nd  11875  ctiunctlemudc  11877  ctiunctlemfo  11879  istps  12126  tpspropd  12130  eltpsg  12134  isms  12549  mspropd  12574  cnlimci  12738
  Copyright terms: Public domain W3C validator