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

Theorem sb6 1572
Description: Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
Assertion
Ref Expression
sb6
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem sb6
StepHypRef Expression
1 sb56 1571 . . 3
21anbi2i 429 . 2
3 df-sb 1438 . 2
4 ax-4 1271 . . 3
54pm4.71ri 369 . 2
62, 3, 53bitr4i 199 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 95   wb 96  wal 1214  wex 1253
This theorem is referenced by:  sb5  1573  sbnv  1574  sbanv  1575  sbi1v  1576  sbi2v  1577  hbs1  1619  2sb6  1634  sb6a  1637  sbalyz  1648  exsb  1652  sbal2  1660
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-5 1215  ax-gen 1218  ax-ie1 1254  ax-ie2 1255  ax-8 1266  ax-11 1268  ax-4 1271  ax-17 1280  ax-i9 1282  ax-ial 1293
This theorem depends on definitions:  df-bi 108  df-sb 1438
  Copyright terms: Public domain W3C validator