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

Theorem sbequ12 1654
 Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ12

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 1651 . 2
2 sbequ2 1652 . 2
31, 2impbid 120 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98  wsb 1645 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-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400 This theorem depends on definitions:  df-bi 110  df-sb 1646 This theorem is referenced by:  sbequ12r  1655  sbequ12a  1656  sbid  1657  ax16  1694  sb8h  1734  sb8eh  1735  sb8  1736  sb8e  1737  ax16ALT  1739  sbco  1842  sbcomxyyz  1846  sb9v  1854  sb6a  1864  mopick  1978  clelab  2162  sbab  2164  cbvralf  2527  cbvrexf  2528  cbvralsv  2544  cbvrexsv  2545  cbvrab  2555  sbhypf  2603  mob2  2721  reu2  2729  reu6  2730  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  cbvreucsf  2910  cbvrabcsf  2911  cbvopab1  3830  cbvopab1s  3832  csbopabg  3835  cbvmpt  3851  opelopabsb  3997  frind  4089  tfis  4306  findes  4326  opeliunxp  4395  ralxpf  4482  rexxpf  4483  cbviota  4872  csbiotag  4895  cbvriota  5478  csbriotag  5480  abrexex2g  5747  opabex3d  5748  opabex3  5749  abrexex2  5751  dfoprab4f  5819  uzind4s  8533  cbvrald  9927  bj-bdfindes  10074  bj-findes  10106
 Copyright terms: Public domain W3C validator