Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq12 Structured version   Visualization version   GIF version

Theorem eleq12 2678
 Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
Assertion
Ref Expression
eleq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))

Proof of Theorem eleq12
StepHypRef Expression
1 eleq1 2676 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 eleq2 2677 . 2 (𝐶 = 𝐷 → (𝐵𝐶𝐵𝐷))
31, 2sylan9bb 732 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606 This theorem is referenced by:  trel  4687  pwnss  4756  epelg  4950  preleq  8397  oemapval  8463  cantnf  8473  wemapwe  8477  nnsdomel  8699  cldval  20637  isufil  21517  issiga  29501  matunitlindf  32577  wepwsolem  36630  aomclem8  36649  umgr2v2enb1  40742
 Copyright terms: Public domain W3C validator