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

Theorem eleqtrd 2132
 Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
eleqtrd.1 (𝜑𝐴𝐵)
eleqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eleqtrd (𝜑𝐴𝐶)

Proof of Theorem eleqtrd
StepHypRef Expression
1 eleqtrd.1 . 2 (𝜑𝐴𝐵)
2 eleqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eleq2d 2123 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 139 1 (𝜑𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259   ∈ wcel 1409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052 This theorem is referenced by:  eleqtrrd  2133  3eltr3d  2136  syl5eleq  2142  syl6eleq  2146  opth1  4000  0nelop  4012  tfisi  4337  ercl  6147  erth  6180  ecelqsdm  6206  phpm  6357  lincmb01cmp  8971  fzopth  9025  fzoaddel2  9150  fzosubel2  9152  fzocatel  9156  zpnn0elfzo1  9165  fzoend  9179  peano2fzor  9189  monoord2  9399  isermono  9400  bcpasc  9633
 Copyright terms: Public domain W3C validator