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

Theorem sbal1 1938
 Description: A theorem used in elimination of disjoint variable conditions on 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 1936 . . . 4
21sbbii 1706 . . 3
3 sbal1yz 1937 . . 3
42, 3syl5bb 191 . 2
5 ax-17 1474 . . 3
65sbco2v 1881 . 2
7 ax-17 1474 . . . 4
87sbco2v 1881 . . 3
98albii 1414 . 2
104, 6, 93bitr3g 221 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 104  wal 1297  wsb 1703 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483 This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator