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

Theorem eleq12d 2108
 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 2107 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq1d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2106 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 177 1 (𝜑 → (𝐴𝐶𝐵𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243   ∈ wcel 1393 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036 This theorem is referenced by:  cbvraldva2  2537  cbvrexdva2  2538  cdeqel  2760  ru  2763  sbcel12g  2865  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  onintexmid  4297  elvvuni  4404  elrnmpt1  4585  smoeq  5905  smores  5907  smores2  5909  iordsmo  5912  nnaordi  6081  nnaordr  6083  ltapig  6436  ltmpig  6437  fzsubel  8923  elfzp1b  8959
 Copyright terms: Public domain W3C validator