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

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

Proof of Theorem sbal1
StepHypRef Expression
1 sbequ12 1465 . . . . 5
21a4s 1296 . . . 4
3 sbequ12 1465 . . . . . 6
43a4s 1296 . . . . 5
54dral2 1436 . . . 4
62, 5bitr3d 177 . . 3
76a1d 20 . 2
8 hba1 1299 . . . . . . 7
98hbsb4 1535 . . . . . 6
10 ax-4 1269 . . . . . . . 8
1110sbimi 1458 . . . . . . 7
1211alimi 1213 . . . . . 6
139, 12syl6 27 . . . . 5
1413adantl 260 . . . 4
15 sb4 1520 . . . . . . . 8
1615al2imi 1216 . . . . . . 7
1716hbnaes 1429 . . . . . 6
18 ax-7 1206 . . . . . 6
1917, 18syl6 27 . . . . 5
20 dveeq2 1503 . . . . . . . . 9
21 alim 1215 . . . . . . . . 9
2220, 21syl9 64 . . . . . . . 8
2322al2imi 1216 . . . . . . 7
24 sb2 1461 . . . . . . 7
2523, 24syl6 27 . . . . . 6
2625hbnaes 1429 . . . . 5
2719, 26sylan9 387 . . . 4
2814, 27impbid 118 . . 3
2928ex 106 . 2
307, 29pm2.61i 736 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 95   wb 96  wal 1204
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-in1 526  ax-in2 527  ax-io 606  ax-3 714  ax-5 1205  ax-7 1206  ax-gen 1207  ax-ie1 1252  ax-ie2 1253  ax-8 1265  ax-10 1266  ax-11 1267  ax-i12 1268  ax-4 1269  ax-17 1284  ax-i9 1288  ax-ial 1293  ax-i5r 1294
This theorem depends on definitions:  df-bi 108  df-tru 1180  df-fal 1181  df-sb 1457
  Copyright terms: Public domain W3C validator