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

Theorem eleqtrd 2167
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 2158 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
41, 3mpbid 146 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1290  wcel 1439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085
This theorem is referenced by:  eleqtrrd  2168  3eltr3d  2171  syl5eleq  2177  syl6eleq  2181  opth1  4072  0nelop  4084  tfisi  4415  ercl  6317  erth  6350  ecelqsdm  6376  phpm  6635  lincmb01cmp  9481  fzopth  9536  fzoaddel2  9665  fzosubel2  9667  fzocatel  9671  zpnn0elfzo1  9680  fzoend  9694  peano2fzor  9704  monoord2  9966  isermono  9967  bcpasc  10235  zfz1isolemiso  10305  fisum0diag2  10902  isumsplit  10946
  Copyright terms: Public domain W3C validator