Description: Lemma for ibladdnc ; cf ibladdlem , whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc . (Contributed by Brendan Leahy, 31-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ibladdnclem.1 | |
|
ibladdnclem.2 | |
||
ibladdnclem.3 | |
||
ibladdnclem.4 | |
||
ibladdnclem.6 | |
||
ibladdnclem.7 | |
||
Assertion | ibladdnclem | |