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

Theorem eleq12d 2186
 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 2185 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq1d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2184 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 187 1 (𝜑 → (𝐴𝐶𝐵𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1314   ∈ wcel 1463 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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111 This theorem is referenced by:  cbvraldva2  2633  cbvrexdva2  2634  cdeqel  2876  ru  2879  sbcel12g  2986  cbvralcsf  3030  cbvrexcsf  3031  cbvreucsf  3032  cbvrabcsf  3033  onintexmid  4455  elvvuni  4571  elrnmpt1  4758  smoeq  6153  smores  6155  smores2  6157  iordsmo  6160  nnaordi  6370  nnaordr  6372  fvixp  6563  cbvixp  6575  mptelixpg  6594  exmidaclem  7028  ltapig  7110  ltmpig  7111  fzsubel  9780  elfzp1b  9817  ennnfonelemg  11811  ennnfonelemp1  11814  ennnfonelemnn0  11830  ctiunctlemu1st  11842  ctiunctlemu2nd  11843  ctiunctlemudc  11845  ctiunctlemfo  11847  istps  12094  tpspropd  12098  eltpsg  12102  isms  12517  mspropd  12542  cnlimci  12694
 Copyright terms: Public domain W3C validator