Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleqtrd Unicode 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  4001  0nelop  4013  tfisi  4338  ercl  6148  erth  6181  ecelqsdm  6207  phpm  6358  lincmb01cmp  8972  fzopth  9026  fzoaddel2  9151  fzosubel2  9153  fzocatel  9157  zpnn0elfzo1  9166  fzoend  9180  peano2fzor  9190  monoord2  9400  isermono  9401  bcpasc  9634
 Copyright terms: Public domain W3C validator