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

Theorem sbal1 1755
Description: A theorem used in elimination of disjoint variable restriction on and by replacing it with a distinctor . (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.)
Assertion
Ref Expression
sbal1
Distinct variable group:   ,
Allowed substitution hints:   (,,)

Proof of Theorem sbal1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sbal 1753 . . . 4
21sbbii 1535 . . 3
3 sbal1yz 1754 . . 3
42, 3syl5bb 179 . 2
5 ax-17 1350 . . 3
65sbco2v 1698 . 2
7 ax-17 1350 . . . 4
87sbco2v 1698 . . 3
98albii 1290 . 2
104, 6, 93bitr3g 209 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 96  wal 1266
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-in2 528  ax-io 609  ax-5 1267  ax-7 1268  ax-gen 1269  ax-ie1 1314  ax-ie2 1315  ax-8 1328  ax-10 1329  ax-11 1330  ax-i12 1331  ax-4 1333  ax-17 1350  ax-i9 1354  ax-ial 1359  ax-i5r 1360
This theorem depends on definitions:  df-bi 108  df-nf 1281  df-sb 1533
  Copyright terms: Public domain W3C validator