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

Theorem sbal1 1826
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 1824 . . . 4
21sbbii 1601 . . 3
3 sbal1yz 1825 . . 3
42, 3syl5bb 179 . 2
5 ax-17 1380 . . 3
65sbco2v 1769 . 2
7 ax-17 1380 . . . 4
87sbco2v 1769 . . 3
98albii 1318 . 2
104, 6, 93bitr3g 209 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 96  wal 1294  wsb 1598
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 529  ax-io 612  ax-5 1295  ax-7 1296  ax-gen 1297  ax-ie1 1342  ax-ie2 1343  ax-8 1357  ax-10 1358  ax-11 1359  ax-i12 1360  ax-bnd 1361  ax-4 1362  ax-17 1380  ax-i9 1384  ax-ial 1389  ax-i5r 1390
This theorem depends on definitions:  df-bi 108  df-nf 1309  df-sb 1599
  Copyright terms: Public domain W3C validator