Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1423 Structured version   Unicode version

Theorem bnj1423 29357
 Description: Technical lemma for bnj60 29368. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1423.1
bnj1423.2
bnj1423.3
bnj1423.4
bnj1423.5
bnj1423.6
bnj1423.7
bnj1423.8
bnj1423.9
bnj1423.10
bnj1423.11
bnj1423.12
bnj1423.13
bnj1423.14
bnj1423.15
bnj1423.16
Assertion
Ref Expression
bnj1423
Distinct variable groups:   ,,,,,   ,   ,   ,,,   ,,,,,   ,,,,,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,,,)   (,,,,)   (,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)   (,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,)

Proof of Theorem bnj1423
StepHypRef Expression
1 bnj1423.1 . . . 4
2 bnj1423.2 . . . 4
3 bnj1423.3 . . . 4
4 bnj1423.4 . . . 4
5 bnj1423.5 . . . 4
6 bnj1423.6 . . . 4
7 bnj1423.7 . . . 4
8 bnj1423.8 . . . 4
9 bnj1423.9 . . . 4
10 bnj1423.10 . . . 4
11 bnj1423.11 . . . 4
12 bnj1423.12 . . . 4
13 bnj1423.13 . . . 4
14 bnj1423.14 . . . 4
15 bnj1423.15 . . . 4
16 bnj1423.16 . . . 4
17 biid 228 . . . 4
18 biid 228 . . . 4
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18bnj1442 29355 . . 3
20 biid 228 . . . 4
21 biid 228 . . . 4
22 biid 228 . . . 4
23 biid 228 . . . 4
24 eqid 2435 . . . 4
251, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20, 21, 22, 23, 24bnj1450 29356 . . 3
2614bnj1424 29147 . . . 4