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

Theorem a9wa9lem8OLD 1414
Description: Obsolete proof of a9wa9lem8 1413 as of 18-Jul-2014.
Hypotheses
Ref Expression
a9wa9.1
a9wa9.2
a9wa9.3
a9wa9.4
a9wa9.5
a9wa9lem8.6
Assertion
Ref Expression
a9wa9lem8OLD
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem a9wa9lem8OLD
StepHypRef Expression
1 ax-17 1402 . . . 4
21a1d 21 . . . 4
31, 2alrimi 1352 . . 3
4 a9wa9.4 . . . . . . 7
5 a9wa9.5 . . . . . . 7
64, 5a9wa9lem3 1407 . . . . . 6
7 a9wa9lem8.6 . . . . . 6
86, 7syl5ibr 144 . . . . 5
98a2i 11 . . . 4
109alimi 1345 . . 3
113, 10syl 14 . 2
124, 5a9wa9lem4 1408 . . . . 5
13 a9wa9.1 . . . . . . . 8
14 a9wa9.2 . . . . . . . 8
1513, 14a9wa9lem3 1407 . . . . . . 7
16 ax-11 1389 . . . . . . 7
1715, 16syl 14 . . . . . 6
18 pm2.27 34 . . . . . . 7
1918al2imi 1348 . . . . . 6
2017, 19syld 39 . . . . 5
2112, 20syl5 27 . . . 4
2221a1d 21 . . 3
23 ax-6 1337 . . . . . . . 8
24 ax-10 1388 . . . . . . . . 9
2524con3i 543 . . . . . . . 8
2623, 25alrimi 1352 . . . . . . 7
2726nalequcoms 1401 . . . . . 6
28 ax-17 1402 . . . . . 6
294, 5, 27, 28a9wa9lem7 1412 . . . . 5
30 ax-6 1337 . . . . . . 7
31 ax-6 1337 . . . . . . 7
3213, 14, 30, 31a9wa9lem7 1412 . . . . . 6
33 ax-12 1393 . . . . . . 7
3433imp 114 . . . . . 6
35 a17d 1403 . . . . . 6
3613, 14, 32, 34, 35a9wa9lem6 1410 . . . . 5
3729, 36hbald 1373 . . . 4
3837ex 107 . . 3
3922, 38pm2.61i 743 . 2
407biimpd 131 . . . . . 6
4140a2i 11 . . . . 5
4241alimi 1345 . . . 4
43 a9wa9.3 . . . . 5
44 con3 550 . . . . . 6
4544al2imi 1348 . . . . 5
4643, 45mtoi 569 . . . 4
47 ax-17 1402 . . . . 5
4847con1i 726 . . . 4
4942, 46, 483syl 17 . . 3
5049alimi 1345 . 2
5111, 39, 50syl56 29 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 96   wb 97  wal 1335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in1 527  ax-in2 528  ax-io 607  ax-5 1336  ax-6 1337  ax-7 1338  ax-gen 1339  ax-8 1387  ax-10 1388  ax-11 1389  ax-i12 1391  ax-4 1392  ax-17 1402
This theorem depends on definitions:  df-bi 109
  Copyright terms: Public domain W3C validator