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

Theorem sb6 1650
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 1649 . . 3
21anbi2i 429 . 2
3 df-sb 1533 . 2
4 ax-4 1333 . . 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 1266  wex 1313
This theorem is referenced by:  sb5  1651  sbnv  1652  sbanv  1653  sbi1v  1655  sbi2v  1656  hbs1  1692  2sb6  1738  sbcom2v  1739  sb6a  1743  sb7af  1748  sbalyz  1754  sbal1yz  1756  exsb  1761  sbal2  1775
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 1267  ax-gen 1269  ax-ie1 1314  ax-ie2 1315  ax-8 1328  ax-11 1330  ax-4 1333  ax-17 1350  ax-i9 1354  ax-ial 1359
This theorem depends on definitions:  df-bi 108  df-sb 1533
  Copyright terms: Public domain W3C validator